max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: avoid Name.quickLt

Browse source 
`Name.quickLt` uses hash code and may produce counterintuitive results
to users.
This commit is contained in:
Leonardo de Moura 2022-01-28 09:48:50 -08:00
parent e5ef61225b
commit 3db640e770
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/ACLt.lean
View file

@ -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!