test(tests/lean/interactive): add tests for coercion and overload info

This commit is contained in:
Leonardo de Moura 2015-01-29 16:39:27 -08:00
parent f04e462bf3
commit c74da8bea2
2 changed files with 68 additions and 0 deletions

View file

@ -0,0 +1,11 @@
VISIT overload_coercions.lean
SYNC 6
open nat num
variable a : nat
variable b : num
variable c : bool
check a + b
check add a c
WAIT
INFO 5
INFO 6

View file

@ -0,0 +1,57 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- TYPE|5|6
-- ACK
-- IDENTIFIER|5|6
a
-- ACK
-- TYPE|5|8
-- ACK
-- OVERLOAD|5|8
num.add #1 #0
--
nat.add #1 #0
-- ACK
-- SYMBOL|5|8
+
-- ACK
-- IDENTIFIER|5|8
nat.add
-- ACK
-- TYPE|5|10
num
-- ACK
-- COERCION|5|10
of_num b
--
-- ACK
-- IDENTIFIER|5|10
b
-- ACK
-- ENDINFO
-- BEGININFO STALE
-- TYPE|6|6
-- ACK
-- OVERLOAD|6|6
num.add
--
nat.add
-- ACK
-- TYPE|6|10
-- ACK
-- IDENTIFIER|6|10
a
-- ACK
-- TYPE|6|12
bool
-- ACK
-- IDENTIFIER|6|12
c
-- ACK
-- ENDINFO