Skip to content

Instantly share code, notes, and snippets.

@chrisamaphone

chrisamaphone/refl.elf

Created March 1, 2024 22:01
Show Gist options
  • Save chrisamaphone/a3a7dcbbe68d01127f72b12284c7bcd0 to your computer and use it in GitHub Desktop.
Save chrisamaphone/a3a7dcbbe68d01127f72b12284c7bcd0 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
refl.elf
nat : type.
z : nat.
s : nat -> nat.
eq : nat -> nat -> type.
refl : eq N N.
%abbrev foo = [x:nat] refl.
% the above typechecks at
% foo : {X1:nat -> nat} {x:nat} eq (X1 x) (X1 x)
% the below fails:
%abbrev bar = [x:nat] refl : eq z x.
% Expected: eq z x
% Inferred: eq (X1 x) (X1 x)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment