epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Add lambda-terms to FOL #231

Open SimonGuilloud opened 4 days ago

SimonGuilloud commented 4 days ago

Reimplement Lisa's syntax to include lambda expressions over first order logic. This will allow, for example, to write directly and efficiently anonymous functions and set comprehensions.