search

epfl-lara / lisa

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

Substitution Rules Param Inference #136

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

Adding one step term and formula rewrite checking

Currently integrated with RightSubstEq as apply2. Needs some more testing. Currently integrating with LeftSubstEq (which sounds like it could be problematic!) and modifying to work with Iff as well.