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

feat: simplify Key.lt

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-24 08:59:38 -08:00
parent 2cf3e197aa
commit 9a4facac29
1 changed files with 8 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Init/Lean/Meta/DiscrTree.lean
View file

@ -78,21 +78,18 @@ def Key.beq : Key → Key → Bool
instance Key.hasBeq : HasBeq Key := ⟨Key.beq⟩
def Key.ctorIdx : Key → Nat
| Key.star => 0
| Key.other => 1
| Key.lit _ => 2
| Key.fvar _ _ => 3
| Key.const _ _ => 4
def Key.lt : Key → Key → Bool
| Key.star, Key.star => false
| Key.star, _ => true
| Key.other, Key.star => false
| Key.other, Key.other => false
| Key.other, _ => true
| Key.lit v₁, Key.lit v₂ => v₁ < v₂
| Key.lit _, Key.const _ _ => true
| Key.lit _, Key.fvar _ _ => true
| Key.lit _, _ => false
| Key.fvar n₁ a₁, Key.fvar n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
| Key.fvar _ _, Key.const _ _ => true
| Key.fvar _ _, _ => false
| Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
| Key.const _ _, _ => false
| k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx
instance Key.hasLess : HasLess Key := ⟨fun a b => Key.lt a b⟩