Fancily-typed variable binding

robrix / path

A lambda calculus to explore type-directed program synthesis.

BSD 3-Clause "New" or "Revised" License

83 stars 2 forks source link

Closed robrix closed 4 years ago

robrix commented 4 years ago

This PR:

Introduces Fin and some machinery to bind/instantiate scopes with finite sets of variables.
Uses Fin for pretty-printing & elaboration.
Defines pretty-printing for Term Core.
🔥s N.
🔥s Name.