Skip to content

Commit

Permalink
Index.Basic: avoid Name.quickCmp when comparing IndexMatchLocations
Browse files Browse the repository at this point in the history
Name.quickCmp makes name comparisons less predictable since for names
containing a numeric part, such as `_uniq.123`, the numeric part is
considered first. This was probably the cause of flakiness in
`AesopTest.RulePattern`, where the order of forward hypotheses would
change due to seemingly unrelated changes.
  • Loading branch information
JLimperg committed Jul 9, 2024
1 parent 0eb81d6 commit cf30d04
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Aesop/Index/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ instance : Ord IndexMatchLocation where
| none, hyp .. => .lt
| hyp .., target => .gt
| hyp .., none => .gt
| hyp ldecl₁, hyp ldecl₂ => ldecl₁.fvarId.name.quickCmp ldecl₂.fvarId.name
| hyp ldecl₁, hyp ldecl₂ => ldecl₁.fvarId.name.cmp ldecl₂.fvarId.name

instance : Hashable IndexMatchLocation where
hash
Expand Down

0 comments on commit cf30d04

Please sign in to comment.