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: explicit type applications #74

Closed robrix closed 4 years ago

robrix commented 5 years ago

E.g.:

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

thing : Bool
thing = id {Bool} true

i.e. the braces indicate that we’re applying an otherwise implicit parameter.

cf #73 for the corresponding syntax for abstractions

robrix commented 4 years ago

Did this in #102 or so.