lean-catLogic / formalization

Formalization of Categorical Logic in the Lean proof assistant
https://lean-catLogic.github.io
3 stars 0 forks source link

Document how the LiftT and HeavyLiftT tactics work #12

Open jacobneu opened 1 year ago

jacobneu commented 1 year ago

In particular, the difference between LiftT, LiftT?, LiftT?!, and LiftT?!! should be documented