A dependently typed programming language, a successor to Idris
Go to file
Edwin Brady 56c0ec5324 Implement inferLambda
This checks lambdas where the type isn't immediately a pi binder. First
normalises, if that doesn't work, just guesses and unifies with the
expected type.
2019-04-07 17:16:44 +01:00
sample Implement inferLambda 2019-04-07 17:16:44 +01:00
src Implement inferLambda 2019-04-07 17:16:44 +01:00
yaffle.ipkg Implement inferLambda 2019-04-07 17:16:44 +01:00