search

epfl-lara / lisa

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

Greedy simplification utilities #145

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

Adding utilities to do a one step greedy substitution from a list. Added a Simplify.exhaustive(also aliased as apply) to run greedy substitution while possible.

May add matching to this system to make it more flexible in a later PR.

sankalpgambhir commented 1 year ago

Definitely, refactoring and cleaning up UnificationUtils and SimpleSimplifier next week!