latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant
MIT License
11 stars 4 forks source link

Delta NBE now working! #19

Closed AustenPrinciple closed 4 years ago

AustenPrinciple commented 4 years ago

No more free-vars, I use the nameless canonical representation for bound variables, as in alpha-norm.