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

Dependent unification #63

Closed robrix closed 5 years ago

robrix commented 5 years ago

I think we could use dependent unification to elaborate implicits (cf #36) &c.

cf A tutorial implementation of dynamic pattern unification, Adam Gundry, Conor McBride cf #36 re: implicits