Improved print debugging on LiftT tactic

lean-catLogic / formalization

Formalization of Categorical Logic in the Lean proof assistant

https://lean-catLogic.github.io

3 stars 0 forks source link

Improved print debugging on LiftT tactic #16

Closed jacobneu closed 1 year ago

jacobneu commented 1 year ago

Now prints an appropriate number of goals at various times, for ease of debugging. Also has count_goals tactic in general for getting the current number of goals (couldn't find anything like this builtin)