cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Annotated lambdas #37

Closed alex-ozdemir closed 4 years ago

alex-ozdemir commented 4 years ago

This PR adds annotated lambdas (using the # sigil). An example is found in the provided test.

This is necessary because we don't actually have annotated lambdas already. The closest thing is %, but they're really more like local declares, and are checked like that (without having function type, using tail recursion, etc.).