Create a gist now

Instantly share code, notes, and snippets.

t ::= terms:
x variable
\x:T .t abstraction
t t application
v ::= values:
\x:T .t abstraction value
T ::= types:
T -> T type of functions
Ⲅ ::= contexts:
φ empty context
Ⲅ, x:T terms variable binding
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment