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

Untyped constraints #88

Closed robrix closed 5 years ago

robrix commented 5 years ago

This PR simplifies the constraint solver by making the constraints untyped. This brings it more into line with Lean’s, while still retaining useful properties w.r.t. constraint solving/elaboration producing sensible results.

robrix commented 5 years ago

Pretty happy with this; among other factors, solving Base.Vector now terminates.