Evaluating bindings in the REPL doesn’t force neutral terms

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 5 years ago

robrix commented 5 years ago

E.g. defining something like:

foo : Nat
foo = z

and then doing

λ: foo

just returns the variable:

foo