fix(tests/lean/interactive): interactive tests expected output, they must include the new '-- BEGINWAIT' messages

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-09 09:47:19 -07:00
parent 187661aa6a
commit 05c6e1461e
5 changed files with 22 additions and 0 deletions

View file

@ -1,3 +1,5 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- SYMBOL|4|22 -- SYMBOL|4|22
Type Type
@ -21,6 +23,8 @@ A
a a
-- ACK -- ACK
-- ENDINFO -- ENDINFO
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- SYMBOL|4|22 -- SYMBOL|4|22
Type Type
@ -44,6 +48,8 @@ B
b b
-- ACK -- ACK
-- ENDINFO -- ENDINFO
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- SYMBOL|5|22 -- SYMBOL|5|22
Type Type
@ -67,6 +73,8 @@ B
b b
-- ACK -- ACK
-- ENDINFO -- ENDINFO
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- SYMBOL|4|22 -- SYMBOL|4|22
Type Type
@ -90,6 +98,10 @@ B
b b
-- ACK -- ACK
-- ENDINFO -- ENDINFO
-- BEGINWAIT
-- ENDWAIT
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- SYMBOL|4|22 -- SYMBOL|4|22
Type Type

View file

@ -6,6 +6,8 @@ Type : Type
-- BEGINEVAL -- BEGINEVAL
Type.{1} : Type.{2} Type.{1} : Type.{2}
-- ENDEVAL -- ENDEVAL
-- BEGINWAIT
-- ENDWAIT
-- BEGINEVAL -- BEGINEVAL
tst.foo.{l_1 l_2} : ?M_1 → ?M_2 → ?M_1 tst.foo.{l_1 l_2} : ?M_1 → ?M_2 → ?M_1
-- ENDEVAL -- ENDEVAL

View file

@ -1,3 +1,5 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- TYPE|9|0 -- TYPE|9|0
eq (tst.foo a b) (tst.foo a b) eq (tst.foo a b) (tst.foo a b)
@ -11,6 +13,8 @@ rfl
-- ENDINFO -- ENDINFO
-- BEGININFO NAY -- BEGININFO NAY
-- ENDINFO -- ENDINFO
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- TYPE|9|0 -- TYPE|9|0
eq (tst.foo a b) (tst.foo a b) eq (tst.foo a b) (tst.foo a b)

View file

@ -1,3 +1,5 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- TYPE|4|0 -- TYPE|4|0
A → B → and A B A → B → and A B

View file

@ -1,3 +1,5 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO -- BEGININFO
-- TYPE|6|6 -- TYPE|6|6
(nat → Prop) → nat (nat → Prop) → nat