issues
search
lean-catLogic
/
formalization
Formalization of Categorical Logic in the Lean proof assistant
https://lean-catLogic.github.io
3
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Improved print debugging on LiftT tactic
#16
jacobneu
closed
1 year ago
0
Abstracted object & morphism counting tactic, made available interactively
#15
jacobneu
closed
1 year ago
0
Implemented fix of has_diamond class
#14
jacobneu
closed
1 year ago
0
Develop theory of syntactic posets (Lindenbaum-Tarski algebras)
#13
jacobneu
opened
1 year ago
0
Document how the LiftT and HeavyLiftT tactics work
#12
jacobneu
opened
1 year ago
0
Abstract diamond modality
#11
jacobneu
closed
1 year ago
1
More proof calculi (and corresponding semantic structures)
#10
jacobneu
opened
1 year ago
0
What's wrong with diamond map?
#9
jacobneu
closed
1 year ago
2
Use mathlib's definition of finite product cat & CCC
#8
jacobneu
opened
1 year ago
0
Improve synCat cleanup & thin_cat.by_thin tactics
#7
jacobneu
opened
1 year ago
1
Move find_it tactic (or better substitute) to generalTactics
#6
jacobneu
closed
1 year ago
1
Abstract PPC
#5
jacobneu
closed
1 year ago
0
Better tactics
#4
jacobneu
closed
1 year ago
1
Proof that downset is a CCC is gross
#3
jacobneu
opened
1 year ago
1
Diamond modality
#2
jacobneu
closed
1 year ago
1
Modular languages
#1
jacobneu
closed
1 year ago
0