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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-21 10:20:42 -07:00
parent 27c3e23c17
commit 19da0229a9
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2,3 +2,5 @@ struct1.lean:9:14: error: expected Type
struct1.lean:12:20: error: expected structure
struct1.lean:15:27: error: field 'toA' has already been declared
struct1.lean:18:27: error: field 'x' from 'B' has already been declared
struct1.lean:22:1: error: invalid field name '_x', identifiers starting with '_' are reserved to the system
struct1.lean:25:3: error: invalid field name '_y', identifiers starting with '_' are reserved to the system