PackageCalculus/Extensions/PackageFormula · package-calculus · Tangled

ryan.freumh.org / package-calculus

The Package Calculus

package-calculus PackageCalculus Extensions PackageFormula

2 folders · 1 file

Ryan Gibb · make reduction helpers public, dedup conflict lifting inverses · 2mo ago

mechanise lifting retractions for all extensions

make reduction helpers public, dedup conflict lifting inverses

Definition.lean

mechanise lifting retractions for all extensions