epfl-lara / lisa

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

Front integration #35

Closed SimonGuilloud closed 2 years ago

SimonGuilloud commented 2 years ago

Integrate front, with changes to the variables structure: MErged Variables and schematic functions of arity 0 Also added special "formula variable" instead of predicates of arity 0, created schematic connectors. All compile, all tests work except in front where some test related to unification and tactics application don't. Front Macros are disactivated for now.