Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-29 17:23 c54d431d

View on Github →

fix(.): unit is now an abbreviation: unit := punit.{1}

Estimated changes

Modified data/encodable.lean

Modified data/equiv.lean

modified def equiv.arrow_empty_unit

modified def equiv.arrow_unit_equiv_unit

modified def equiv.bool_equiv_unit_sum_unit

modified def equiv.empty_arrow_equiv_unit

modified def equiv.false_arrow_equiv_unit

modified def equiv.nat_equiv_nat_sum_unit

modified def equiv.nat_sum_unit_equiv_nat

modified def equiv.option_equiv_sum_unit

modified def equiv.prod_unit

modified theorem equiv.prod_unit_apply

added def equiv.punit_equiv_punit

modified def equiv.unit_arrow_equiv

modified def equiv.unit_prod

modified theorem equiv.unit_prod_apply

Modified set_theory/ordinal.lean

modified theorem ordinal.is_normal.limit_le