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

fix(tests/lean): fix tests that print patterns

Browse source
This commit is contained in:
Daniel Selsam 2015-12-07 11:51:44 -08:00 committed by Leonardo de Moura
parent 18f224c420
commit 0f76e33724
4 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/bad_pattern.lean.expected.out
View file

@ -2,13 +2,16 @@ bad_pattern.lean:9:33: error: invalid pattern hint, pattern hints must be applic
theorem tst₀ [forward] : ∀ (x : ℕ), P x :=
sorry
(multi-)patterns:
?M_1 : ℕ
{P ?M_1}
theorem tst₁ [forward] : ∀ (x : ℕ), (:P x:) :=
sorry
(multi-)patterns:
?M_1 : ℕ
{P ?M_1}
theorem tst₃ [forward] : ∀ (x : ℕ), P (:id x:) :=
sorry
(multi-)patterns:
?M_1 : ℕ
{P ?M_1}
bad_pattern.lean:20:0: error: pattern inference failed for [forward] annotation, (solution: provide pattern hints using the notation '(: t :)' )

1
tests/lean/pattern_bug1.lean.expected.out
View file

@ -1,4 +1,5 @@
definition H [forward] : ∀ (a : A), (:P a:) → Exists (R a) :=
sorry
(multi-)patterns:
?M_1 : A
{P ?M_1}

3
tests/lean/pattern_hint1.lean.expected.out
View file

@ -1,13 +1,16 @@
definition foo₁ [forward] : ∀ (x : ℕ), f x ∧ g x :=
sorry
(multi-)patterns:
?M_1 : ℕ
{f ?M_1}
{g ?M_1}
definition foo₂ [forward] : ∀ (x : ℕ), (:f x:) ∧ g x :=
sorry
(multi-)patterns:
?M_1 : ℕ
{f ?M_1}
definition foo₃ [forward] : ∀ (x : ℕ), (:f (id x):) ∧ g x :=
sorry
(multi-)patterns:
?M_1 : ℕ
{f ?M_1}

3
tests/lean/redundant_pattern.lean.expected.out
View file

@ -1,4 +1,5 @@
definition foo [forward] : ∀ (m n k : ℕ), P (f m) → P (g n) → P (f k) → P k ∧ R (g m) (f n) ∧ P (g m) ∧ P (f n) :=
λ (m n k : ℕ), sorry
(multi-)patterns:
{P ?M_1, R (g ?M_2) (f ?M_3)}
?M_1 : ℕ, ?M_2 : ℕ, ?M_3 : ℕ
{P ?M_3, R (g ?M_1) (f ?M_2)}