Skip to content

fix: recognize opaque constants of unit-like types as definitionally equal - #14550

Open
kernelpanic888 wants to merge 5 commits into
leanprover:masterfrom
kernelpanic888:codex/fix-opaque-unit-defeq-14348
Open

fix: recognize opaque constants of unit-like types as definitionally equal#14550
kernelpanic888 wants to merge 5 commits into
leanprover:masterfrom
kernelpanic888:codex/fix-opaque-unit-defeq-14348