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

test(tests/lean/inaccessible2): add more invalid pattern tests

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-28 07:22:31 -07:00
parent ae63821cdb
commit 0ed61c97c9
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/inaccessible2.lean
View file

@ -5,3 +5,9 @@ inductive imf {A B : Type} (f : A → B) : B → Type
definition inv_1 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| .(f .a) (imf.mk .f a) := a -- Error inaccessible annotation inside inaccessible annotation
definition inv_2 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| .(f a) (let x := (imf.mk .f a) in x) := a -- Error invalid occurrence of 'let' expression
definition inv_3 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| .(f a) ((λ (x : imf f b), x) (imf.mk .f a)) := a -- Error invalid occurrence of 'lambda' expression

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

@ -1 +1,3 @@
inaccessible2.lean:7:7: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
inaccessible2.lean:10:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
inaccessible2.lean:13:13: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term