Syntax sugar: bind parameters on the lhs of definitions

robrix / path

A lambda calculus to explore type-directed program synthesis.

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

83 stars 2 forks source link

Open robrix opened 5 years ago

robrix commented 5 years ago

E.g.:

id : ∀ a : Type . a -> a
id _ a = a

as syntax sugar for

id : ∀ a : Type . a -> a
id = \ _ a . a

robrix commented 5 years ago

We might also want to allow patterns on the lhs once we have case expressions (cf #37) for pattern-matching.