Add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
389f23f356
commit
a5adddaf14
6 changed files with 67 additions and 3 deletions
2
.gitignore
vendored
2
.gitignore
vendored
|
@ -1,5 +1,6 @@
|
|||
*~
|
||||
.lean_trace
|
||||
*.produced.out
|
||||
a.out
|
||||
build
|
||||
GPATH
|
||||
|
@ -9,4 +10,3 @@ GTAGS
|
|||
Makefile
|
||||
*.cmake
|
||||
CMakeFiles/
|
||||
|
||||
|
|
17
tests/lean/ex2.lean
Normal file
17
tests/lean/ex2.lean
Normal file
|
@ -0,0 +1,17 @@
|
|||
(* comment *)
|
||||
(* (* nested comment *) *)
|
||||
Show true
|
||||
Set lean::pp::notation false
|
||||
Show true && false
|
||||
Variable a : Bool
|
||||
Variable a : Bool
|
||||
Variable b : Bool
|
||||
Show a && b
|
||||
Variable A : Type
|
||||
Check a && A
|
||||
Show Environment 1
|
||||
Show Options
|
||||
Set lean::p::notation true
|
||||
Set lean::pp::notation 10
|
||||
Set lean::pp::notation true
|
||||
Show a && b
|
20
tests/lean/ex2.lean.expected.out
Normal file
20
tests/lean/ex2.lean.expected.out
Normal file
|
@ -0,0 +1,20 @@
|
|||
⊤
|
||||
Set option: lean::pp::notation
|
||||
and true false
|
||||
Assumed: a
|
||||
Error (line: 7, pos: 0) invalid object declaration, environment already has an object named 'a'
|
||||
Assumed: b
|
||||
and a b
|
||||
Assumed: A
|
||||
Error (line: 11, pos: 11) type mismatch at application argument 2 of
|
||||
and a A
|
||||
expected type
|
||||
Bool
|
||||
given type
|
||||
[36mType[0m
|
||||
[34mVariable[0m A : [36mType[0m
|
||||
⟨lean::pp::notation ↦ false⟩
|
||||
Error (line: 14, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
|
||||
Error (line: 15, pos: 23) invalid option value, given option is not an integer
|
||||
Set option: lean::pp::notation
|
||||
a ∧ b
|
9
tests/lean/ex3.lean
Normal file
9
tests/lean/ex3.lean
Normal file
|
@ -0,0 +1,9 @@
|
|||
Variable myeq : Pi (A : Type), A -> A -> Bool
|
||||
Show myeq _ true false
|
||||
Variable T : Type
|
||||
Variable a : T
|
||||
Check myeq _ true a
|
||||
Variable myeq2 {A:Type} (a b : A) : Bool
|
||||
Infix 50 === : myeq2
|
||||
Set lean::pp::implicit true
|
||||
Check true === a
|
18
tests/lean/ex3.lean.expected.out
Normal file
18
tests/lean/ex3.lean.expected.out
Normal file
|
@ -0,0 +1,18 @@
|
|||
Assumed: myeq
|
||||
myeq Bool ⊤ ⊥
|
||||
Assumed: T
|
||||
Assumed: a
|
||||
Error (line: 5, pos: 6) type mismatch at application argument 3 of
|
||||
myeq Bool ⊤ a
|
||||
expected type
|
||||
Bool
|
||||
given type
|
||||
T
|
||||
Assumed: myeq2
|
||||
Set option: lean::pp::implicit
|
||||
Error (line: 9, pos: 15) type mismatch at application argument 3 of
|
||||
myeq2::explicit Bool ⊤ a
|
||||
expected type
|
||||
Bool
|
||||
given type
|
||||
T
|
|
@ -11,11 +11,11 @@ else
|
|||
fi
|
||||
NUM_ERRORS=0
|
||||
for f in `ls *.lean`; do
|
||||
echo $f
|
||||
echo "-- testing $f"
|
||||
$LEAN $f > $f.produced.out
|
||||
if test -f $f.expected.out; then
|
||||
if diff $f.produced.out $f.expected.out; then
|
||||
echo "-- $f checked"
|
||||
echo "-- checked"
|
||||
else
|
||||
echo "ERROR: file $f.produced.out does not match $f.expected.out"
|
||||
NUM_ERRORS=$(($NUM_ERRORS+1))
|
||||
|
|
Loading…
Reference in a new issue