search

robrix / path

A lambda calculus to explore type-directed program synthesis.
BSD 3-Clause "New" or "Revised" License
83 stars 2 forks source link

Declarations w/o definitions typecheck but can’t be evaluated #70

Open robrix opened 5 years ago

robrix commented 5 years ago

E.g. if you declare a binding and use it to define another binding:

foo : Nat

bar : Nat
bar = id Nat foo

then we can typecheck bar successfully but can’t really evaluate it because it’s free in the environment.