Tests for proof tactics (!106) · Merge requests · LARA / lisa

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/tactic-tests into main Dec 02, 2022

Adding tests for proof tactics, since it seems we currently miss some errors during changes!

Progress: ✔ Hypo, Rewrite (WIP to use EqvChecker test functions), Cut ✔ Left rules ✔ Right rules ✔ Structural rules

Other changes to facilitate things: :1st_place_medal: unwrapTactic utility to call other tactics safely

Issues: The new tests in this PR will fail till I fix these (eventually) ✔ LeftExists checking ✔ OCBSL/Weakening leniency ✔ InstantiateForall not working due to argument type mismatch -> changed it to accept a sequent and check against it

Tests for proof tactics

Merge request reports