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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-07 15:57:02 -07:00
parent 734d8af3b9
commit 38f66c580b
4 changed files with 29 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
tests/compiler/array_test.lean.expected.out
View file

@ -1,22 +1,22 @@
[]
#[]
0
[0, 1, 2, 3]
[10, 11, 12, 13]
#[0, 1, 2, 3]
#[10, 11, 12, 13]
4
[10, 11, 12]
[10, 11, 12, 13, 100]
[10, 11, 12]
[3, 4, 5, 6]
[2, 3]
[]
[]
[3, 4]
[4, 3, 2, 1]
[]
[3, 2, 1]
[2, 4]
[2, 4]
[1, 3, 5]
[3, 4]
[]
[1, 2, 3, 4]
#[10, 11, 12]
#[10, 11, 12, 13, 100]
#[10, 11, 12]
#[3, 4, 5, 6]
#[2, 3]
#[]
#[]
#[3, 4]
#[4, 3, 2, 1]
#[]
#[3, 2, 1]
#[2, 4]
#[2, 4]
#[1, 3, 5]
#[3, 4]
#[]
#[1, 2, 3, 4]

2
tests/compiler/qsortBadLt.lean.expected.out
View file

@ -1 +1 @@
[1, 2]
#[1, 2]

12
tests/compiler/termparsertest1.lean.expected.out
View file

@ -166,11 +166,13 @@ fun (Prod.mk x y) => f y x
(null (Term.structInstField `fst ":=" (numLit "10")) "," (Term.structInstSource ".." (null)))
"}")
a[i]
(Term.array (Term.id `a (null)) "[" (Term.id `i (null)) "]")
(Term.arrayRef (Term.id `a (null)) "[" (Term.id `i (null)) "]")
f [10, 20]
(Term.app (Term.id `f (null)) (Term.list "[" (null (numLit "10") "," (numLit "20")) "]"))
(Term.app (Term.id `f (null)) (Term.listLit "[" (null (numLit "10") "," (numLit "20")) "]"))
g a[x+2]
(Term.app (Term.id `g (null)) (Term.array (Term.id `a (null)) "[" (Term.add (Term.id `x (null)) "+" (numLit "2")) "]"))
(Term.app
(Term.id `g (null))
(Term.arrayRef (Term.id `a (null)) "[" (Term.add (Term.id `x (null)) "+" (numLit "2")) "]"))
g f.a.1.2.bla x.1.a
(Term.app
(Term.app
@ -384,7 +386,7 @@ let x[i].y := f 10; x
(Term.let
"let"
(Term.letPatDecl
(Term.proj (Term.array (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y)
(Term.proj (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y)
(null)
":="
(Term.app (Term.id `f (null)) (numLit "10")))
@ -394,7 +396,7 @@ let x[i] := f 20; x
(Term.let
"let"
(Term.letPatDecl
(Term.array (Term.id `x (null)) "[" (Term.id `i (null)) "]")
(Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]")
(null)
":="
(Term.app (Term.id `f (null)) (numLit "20")))

2
tests/lean/binsearch.lean.expected.out
View file

@ -1,4 +1,4 @@
[(9, false), (8, true), (7, false), (6, true), (5, false), (4, true), (3, false), (2, true), (1, false), (0, true)]
#[(9, false), (8, true), (7, false), (6, true), (5, false), (4, true), (3, false), (2, true), (1, false), (0, true)]
>> 0 ==> (some (0, true))
>> 1 ==> (some (1, false))
>> 2 ==> (some (2, true))