From 0ed61c97c940e015dcf1f61ccbbb6a3a9fedd7bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Aug 2016 07:22:31 -0700 Subject: [PATCH] test(tests/lean/inaccessible2): add more invalid pattern tests --- tests/lean/inaccessible2.lean | 6 ++++++ tests/lean/inaccessible2.lean.expected.out | 2 ++ 2 files changed, 8 insertions(+) diff --git a/tests/lean/inaccessible2.lean b/tests/lean/inaccessible2.lean index 094d22e646..757c50cacd 100644 --- a/tests/lean/inaccessible2.lean +++ b/tests/lean/inaccessible2.lean @@ -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 diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out index 849336f31f..ddd241c93a 100644 --- a/tests/lean/inaccessible2.lean.expected.out +++ b/tests/lean/inaccessible2.lean.expected.out @@ -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