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

chore: remove unnecessary annotations

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-23 20:42:59 -07:00
parent 6f6bb02bcd
commit 1b7f7e9d39
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/matchWithSearch.lean
View file

@ -26,21 +26,21 @@ inductive almostNode : Nat → Type
| V {h c} (node:rbnode h c) : almostNode h
open almostNode
def balanceRR {h c} (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
def balanceRR (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
match h, c, left, right with
| _, _, left, HR c => RR left y c
| _, _, R a x b, HB c => LR (R a x b) y c
| _, _, B a x b, HB c => V (R (B a x b) y c)
| _, _, Leaf, HB c => V (R Leaf y c)
def balanceRR' {h c} (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
def balanceRR' (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
match h, c, right, left with
| _, _, HR c, left => RR left y c
| _, _, HB c, R a x b => LR (R a x b) y c
| _, _, HB c, B a x b => V (R (B a x b) y c)
| _, _, HB c, Leaf => V (R Leaf y c)
def balanceRR'' {h c} (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
def balanceRR'' (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
match left, right with
| left, HR c => RR left y c
| R a x b, HB c => LR (R a x b) y c