Logical equivalences should have definitions of concrete proofs first, and then
have accompanying theorems derived through Proposition.equiv.toProp.
|
/- TODO: Proof-relevant logical equivalences. |
|
|
|
Logical equivalences should have definitions of concrete proofs first, and then |
|
have accompanying theorems derived through `Proposition.equiv.toProp`. |
|
labels: logic |
|
-/ |
Logical equivalences should have definitions of concrete proofs first, and then
have accompanying theorems derived through
Proposition.equiv.toProp.cslib/Cslib/Logics/LinearLogic/CLL/Basic.lean
Lines 275 to 280 in 03c480f