From 3db640e770ea7a789926980b800cd8065528b0a0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Jan 2022 09:48:50 -0800 Subject: [PATCH] chore: avoid `Name.quickLt` `Name.quickLt` uses hash code and may produce counterintuitive results to users. --- src/Lean/Meta/ACLt.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean index 1103595e7b..bcd9c7a4d3 100644 --- a/src/Lean/Meta/ACLt.lean +++ b/src/Lean/Meta/ACLt.lean @@ -96,10 +96,10 @@ where match a with -- Atomic | Expr.bvar i .. => i < b.bvarIdx! - | Expr.fvar id .. => Name.quickLt id.name b.fvarId!.name - | Expr.mvar id .. => Name.quickLt id.name b.mvarId!.name + | Expr.fvar id .. => Name.lt id.name b.fvarId!.name + | Expr.mvar id .. => Name.lt id.name b.mvarId!.name | Expr.sort u .. => Level.normLt u b.sortLevel! - | Expr.const n .. => Name.quickLt n b.constName! -- We igore the levels + | Expr.const n .. => Name.lt n b.constName! -- We igore the levels | Expr.lit v .. => Literal.lt v b.litValue! -- Composite | Expr.proj _ i e .. => if i != b.projIdx! then i < b.projIdx! else lt e b.projExpr!