Commit 2023-10-19 09:56 c1696eec

View on Github →

style: CoeFun for PFunctor.Obj & MvPFunctor.Obj (#7526)

Estimated changes

modified def MvPFunctor.comp.get
modified theorem MvPFunctor.comp.get_map
modified theorem MvPFunctor.comp.get_mk
modified def MvPFunctor.comp.mk
modified theorem MvPFunctor.comp.mk_get
modified def MvPFunctor.comp
modified def MvPFunctor.const.get
modified theorem MvPFunctor.const.get_map
modified theorem MvPFunctor.const.get_mk
modified def MvPFunctor.const.mk
modified theorem MvPFunctor.const.mk_get
modified theorem MvPFunctor.id_map
modified theorem MvPFunctor.liftP_iff
modified theorem MvPFunctor.liftR_iff
modified def MvPFunctor.map
modified def MvPFunctor.M.corec
modified def MvPFunctor.M.dest
modified theorem MvPFunctor.M.dest_corec
modified def MvPFunctor.M.mk
modified def MvPFunctor.wDest'
modified theorem MvPFunctor.wDest'_wMk'
modified def MvPFunctor.wMk'
modified def PFunctor.Obj.iget
modified def PFunctor.Obj
modified def PFunctor.W.dest
modified theorem PFunctor.W.dest_mk
modified def PFunctor.W.mk
modified def PFunctor.comp.get
modified def PFunctor.comp.mk
modified theorem PFunctor.fst_map
modified theorem PFunctor.iget_map
modified theorem PFunctor.liftp_iff
modified theorem PFunctor.liftr_iff
modified def PFunctor.map
modified theorem PFunctor.M.casesOn_mk
modified theorem PFunctor.M.cases_mk
modified def PFunctor.M.corec'
modified def PFunctor.M.corecOn
modified theorem PFunctor.M.corec_def
modified theorem PFunctor.M.corec_unique
modified def PFunctor.M.corec₁
modified def PFunctor.M.dest
modified theorem PFunctor.M.dest_corec
modified theorem PFunctor.M.dest_mk
modified theorem PFunctor.M.head_mk
modified theorem PFunctor.M.ichildren_mk
modified theorem PFunctor.M.mk_inj
modified def MvQPF.Cofix.corec'
modified def MvQPF.Prj.abs
modified def MvQPF.Prj.repr