search

epfl-lara / lisa

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

Easy-tactics API for Forall Instantiation #68

Closed sankalpgambhir closed 2 years ago

sankalpgambhir commented 2 years ago

Added API for forall instantiation as a simple deduced step.

Currently some code is (unfortunately in a not so pretty manner) repeated between simultaneous and single quantifier instantiation due to issues with composing deduced tactics. This may be improved in the future by having the multiple instantiations compose single ones into a DoubleStep based Proof object.