michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/interactive): adjust test output to reflect new features

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-17 15:23:53 -07:00
parent dcc8f4e4fc
commit 13af81d554
1 changed files with 60 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
tests/lean/interactive/in1.input.expected.out
View file

@ -1,63 +1,123 @@
DONE
-- BEGININFO
-- SYMBOL|4|22
Type
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- TYPE|4|41
Type
-- ACK
-- IDENTIFIER|4|41
B
-- ACK
-- TYPE|4|47
A
-- ACK
-- IDENTIFIER|4|47
a
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- SYMBOL|4|22
Type
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- TYPE|4|41
Type
-- ACK
-- IDENTIFIER|4|41
B
-- ACK
-- TYPE|4|47
B
-- ACK
-- IDENTIFIER|4|47
b
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- SYMBOL|5|22
Type
-- ACK
-- TYPE|5|33
Type
-- ACK
-- IDENTIFIER|5|33
A
-- ACK
-- TYPE|5|41
Type
-- ACK
-- IDENTIFIER|5|41
B
-- ACK
-- TYPE|5|47
B
-- ACK
-- IDENTIFIER|5|47
b
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- SYMBOL|4|22
Type
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- TYPE|4|41
Type
-- ACK
-- IDENTIFIER|4|41
B
-- ACK
-- TYPE|4|47
B
-- ACK
-- IDENTIFIER|4|47
b
-- ACK
-- ENDINFO
simple.lean:4:0: error: command expected
simple.lean:5:37: error: unknown identifier 'foo'
DONE
DONE
-- BEGININFO
-- SYMBOL|4|22
Type
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- TYPE|4|41
Type
-- ACK
-- IDENTIFIER|4|41
B
-- ACK
-- TYPE|4|47
B
-- ACK
-- IDENTIFIER|4|47
b
-- ACK
-- ENDINFO