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

Syntax sugar: syntax for explicitized type abstractions #73

Closed robrix closed 4 years ago

robrix commented 5 years ago

E.g. something like this:

id : { a : Type } -> a -> a
id = \ {A} a . a

i.e. use braces around the param to explicitize the type abstraction (which would otherwise be implicitly generated).

robrix commented 4 years ago

Did this in #102 or so.