Commit 2023-09-22 07:38 40fe5127

View on Github →

chore: Remove Cat suffixes (#3730) These names needn't change in the first place.

Estimated changes

added def BoolRing.Iso.mk
added theorem BoolRing.coe_of
added def BoolRing.of
added def BoolRing
deleted def BoolRingCat.Iso.mk
deleted theorem BoolRingCat.coe_of
deleted def BoolRingCat.of
deleted def BoolRingCat
added theorem BddDistLat.coe_of
added def BddDistLat.dual
added def BddDistLat.of
added structure BddDistLat
deleted theorem BddDistLatCat.coe_of
deleted def BddDistLatCat.dual
deleted def BddDistLatCat.of
deleted structure BddDistLatCat
added def BddLat.Iso.mk
added theorem BddLat.coe_of
added def BddLat.dual
added def BddLat.dualEquiv
added def BddLat.of
added structure BddLat
added def latToBddLat
deleted def BddLatCat.Iso.mk
deleted theorem BddLatCat.coe_of
deleted def BddLatCat.dual
deleted def BddLatCat.dualEquiv
deleted def BddLatCat.of
deleted structure BddLatCat
deleted def latToBddLatCat
added def BddOrd.Iso.mk
added theorem BddOrd.coe_of
added def BddOrd.dual
added def BddOrd.dualEquiv
added def BddOrd.of
added structure BddOrd
deleted def BddOrdCat.Iso.mk
deleted theorem BddOrdCat.coe_of
deleted def BddOrdCat.dual
deleted def BddOrdCat.dualEquiv
deleted def BddOrdCat.of
deleted structure BddOrdCat
added def BoolAlg.Iso.mk
added theorem BoolAlg.coe_of
added def BoolAlg.dual
added def BoolAlg.of
added def BoolAlg
deleted def BoolAlgCat.Iso.mk
deleted theorem BoolAlgCat.coe_of
deleted def BoolAlgCat.dual
deleted def BoolAlgCat.of
deleted def BoolAlgCat
added theorem CompleteLat.coe_of
added def CompleteLat.dual
added def CompleteLat.of
added def CompleteLat
deleted theorem CompleteLatCat.coe_of
deleted def CompleteLatCat.dual
deleted def CompleteLatCat.of
deleted def CompleteLatCat
added def DistLat.Iso.mk
added theorem DistLat.coe_of
added def DistLat.dual
added def DistLat.of
added def DistLat
deleted def DistLatCat.Iso.mk
deleted theorem DistLatCat.coe_of
deleted def DistLatCat.dual
deleted def DistLatCat.of
deleted def DistLatCat
added def FinBddDistLat.of
added structure FinBddDistLat
deleted def FinBddDistLatCat.of
deleted structure FinBddDistLatCat
added theorem FinBoolAlg.coe_of
added def FinBoolAlg.dual
added def FinBoolAlg.of
added structure FinBoolAlg
deleted theorem FinBoolAlgCat.coe_of
deleted def FinBoolAlgCat.dual
deleted def FinBoolAlgCat.of
deleted structure FinBoolAlgCat
added def Frm.Iso.mk
added theorem Frm.coe_of
added def Frm.of
added def Frm
deleted def FrmCat.Iso.mk
deleted theorem FrmCat.coe_of
deleted def FrmCat.of
deleted def FrmCat
deleted def topCatOpToFrameCat
added def topCatOpToFrm
added def HeytAlg.Iso.mk
added theorem HeytAlg.coe_of
added def HeytAlg.of
added def HeytAlg
deleted def HeytAlgCat.Iso.mk
deleted theorem HeytAlgCat.coe_of
deleted def HeytAlgCat.of
deleted def HeytAlgCat
added def Lat.Iso.mk
added theorem Lat.coe_of
added def Lat.dual
added def Lat.dualEquiv
added def Lat.of
added def Lat
deleted def LatCat.Iso.mk
deleted theorem LatCat.coe_of
deleted def LatCat.dual
deleted def LatCat.dualEquiv
deleted def LatCat.of
deleted def LatCat
added def LinOrd.Iso.mk
added theorem LinOrd.coe_of
added def LinOrd.dual
added def LinOrd.dualEquiv
added def LinOrd.of
added def LinOrd
deleted def LinOrdCat.Iso.mk
deleted theorem LinOrdCat.coe_of
deleted def LinOrdCat.dual
deleted def LinOrdCat.dualEquiv
deleted def LinOrdCat.of
deleted def LinOrdCat
added def PartOrd.Iso.mk
added theorem PartOrd.coe_of
added def PartOrd.dual
added def PartOrd.of
added def PartOrd
deleted def PartOrdCat.Iso.mk
deleted theorem PartOrdCat.coe_of
deleted def PartOrdCat.dual
deleted def PartOrdCat.of
deleted def PartOrdCat
added def preordToPartOrd
added def Preord.Iso.mk
added theorem Preord.coe_of
added def Preord.dual
added def Preord.dualEquiv
added def Preord.of
added def Preord
deleted def PreordCat.Iso.mk
deleted theorem PreordCat.coe_of
deleted def PreordCat.dual
deleted def PreordCat.dualEquiv
deleted def PreordCat.of
deleted def PreordCat
deleted def preordCatToCat
added def preordToCat
modified def alexDiscEquivPreord
modified def topToPreord