Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kernelpanic888 wants to merge 5 commits into
base: master
Choose a base branch
from
+12 −1
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
d288619
fix: recognize opaque constants of unit-like types
kernelpanic888 Jul 25, 2026
71e4ada
test: cover opaque unit-like constant equality
kernelpanic888 Jul 25, 2026
0ebf6be
fix: restore opaque unit-like fallback
osalkutsan-godaddy Jul 30, 2026
2fdb446
fix: limit constant fallback to unit-like types
osalkutsan-godaddy Jul 30, 2026
181faf7
chore: merge master into fix branch
kernelpanic888 Sep 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion src/Lean/Meta/ExprDefEq.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2426,7 +2426,10 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
return true
if t.isConst && s.isConst then
if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
if t.constName! == s.constName! then
isListLevelDefEqAux t.constLevels! s.constLevels!
else
isDefEqUnitLike t s
else if (← pure t.isApp <&&> pure s.isApp) then
if (← isDefEqApp t s) then return true
isDefEqAppFallback t s
Expand Down
8 changes: 8 additions & 0 deletions tests/elab/14348.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
module

/-! Regression test for issue #14348: opaque constants of a unit-like type are definitionally equal. -/

opaque a : Unit
opaque b : Unit

example : a = b := rfl
Loading