Skip to content

Easy-tactics API for Forall Instantiation

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/easy-inst-forall into easy-tactics

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.

Merge request reports