From e36b981cbe8f1782e955393c368fe2fce324f524 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 11 Jul 2026 10:02:12 -0400 Subject: [PATCH] fix(Order/Notation): unify at correct transparency in sup/inf delaborators --- Mathlib/Order/Notation.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/Order/Notation.lean b/Mathlib/Order/Notation.lean index 9cd2fb4f2df3af..2adee424716281 100644 --- a/Mathlib/Order/Notation.lean +++ b/Mathlib/Order/Notation.lean @@ -100,13 +100,12 @@ private meta def hasLinearOrder (u : Level) (α : Q(Type u)) (cls : Q(Type u → MetaM Bool := do try withNewMCtxDepth do - -- `isDefEq` may call type class search to instantiate `mvar`, so we need the local instances - -- In Lean 4.19 the pretty printer clears local instances, so we re-add them here. - -- TODO(Jovan): remove + -- `isDefEq` may call type class search to instantiate `mvar`, so we need the local instances. + -- Unfortunately, we need to set the local instances manually. withLocalInstances (← getLCtx).decls.toList.reduceOption do let mvar ← mkFreshExprMVarQ q($(linearOrderExpr u) $α) (kind := .synthetic) let inst' : Q($cls $α) := q($toCls $α $mvar) - isDefEq inst inst' + withReducibleAndInstances <| isDefEq inst inst' catch _ => -- For instance, if `LinearOrder` is not yet imported. return false