Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/simplest_fix.md

Created June 27, 2023 05:04
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save EduardoRFS/b2f6f5602395b6936312f15c40a77de5 to your computer and use it in GitHub Desktop.
Save EduardoRFS/b2f6f5602395b6936312f15c40a77de5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
simplest_fix.md 
Γ, x : %self(x). T |- T : Type
------------------------------
%self(x). T : Type

Γ, x : %self(x). T |- M : T[x := %fix(x) : T. M]
------------------------------------------------
%fix(x) : T. M : %self(x). T

Γ |- M : %self(x). T
---------------------
%unroll M : T[x := M]

Γ |- N : P (%unroll (%fix(x) : T. M))
---------------------------------------
%expand(N) : P (M[x := %fix(x) : T. M])

----------------
%expand(N) === N
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment