search

lean-catLogic / formalization

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

Better tactics #4

Closed jacobneu closed 1 year ago

jacobneu commented 1 year ago

The lifting derivation tactics (as originally written) were a bit blunt, e.g. using a ton of repeats. The goal with this PR is to improve them by writing them in a more principled monadic style.

jacobneu commented 1 year ago

Moved some further work to issues #6 and #7. Going ahead with merge.