Skip to content

chore(Data/PFunctor): fix defeq abuse in PFunctor.Obj - #43056

Open
plp127 wants to merge 9 commits into
leanprover-community:masterfrom
plp127:aliu/PFunctor-Obj
Open

chore(Data/PFunctor): fix defeq abuse in PFunctor.Obj#43056
plp127 wants to merge 9 commits into
leanprover-community:masterfrom
plp127:aliu/PFunctor-Obj

`Sigma.snd` is fine now

5c64610
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Aug 24, 2026 in 9m 5s