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

chore(tests/lean/inductive_sorry): remove test

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-15 20:37:53 -07:00
parent cddf5f081d
commit 16392fda7d
2 changed files with 0 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/inductive_sorry.lean
View file

@ -1,12 +0,0 @@
inductive foo (A : sorry → ℕ)
| mk : foo
inductive foo : sorry → ℕ
| mk : foo 0
inductive foo
| mk : sorry → foo
structure foo (A : sorry → ℕ) := (x : ℕ)
structure foo : Type := (x : bool → sorry)

5
tests/lean/inductive_sorry.lean.expected.out
View file

@ -1,5 +0,0 @@
inductive_sorry.lean:1:0: error: type of parameter 'A' contains 'sorry'
inductive_sorry.lean:4:0: error: type of parameter 'foo' contains 'sorry'
inductive_sorry.lean:7:0: error: constructor 'foo.mk' contains 'sorry'
inductive_sorry.lean:10:0: error: type of parameter 'A' contains 'sorry'
inductive_sorry.lean:12:0: error: field 'x' contains 'sorry'