From 0f76e3372433b15b7ee262ff643b88d58d4ea0c4 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 7 Dec 2015 11:51:44 -0800
Subject: [PATCH] fix(tests/lean): fix tests that print patterns

---
 tests/lean/bad_pattern.lean.expected.out       | 3 +++
 tests/lean/pattern_bug1.lean.expected.out      | 1 +
 tests/lean/pattern_hint1.lean.expected.out     | 3 +++
 tests/lean/redundant_pattern.lean.expected.out | 3 ++-
 4 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/tests/lean/bad_pattern.lean.expected.out b/tests/lean/bad_pattern.lean.expected.out
index 05f0463ab..27145d1fe 100644
--- a/tests/lean/bad_pattern.lean.expected.out
+++ b/tests/lean/bad_pattern.lean.expected.out
@@ -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 :)' )
diff --git a/tests/lean/pattern_bug1.lean.expected.out b/tests/lean/pattern_bug1.lean.expected.out
index 1964b92f5..66899cd7f 100644
--- a/tests/lean/pattern_bug1.lean.expected.out
+++ b/tests/lean/pattern_bug1.lean.expected.out
@@ -1,4 +1,5 @@
 definition H [forward] : ∀ (a : A), (:P a:) → Exists (R a) :=
 sorry
 (multi-)patterns:
+?M_1 : A
 {P ?M_1}
diff --git a/tests/lean/pattern_hint1.lean.expected.out b/tests/lean/pattern_hint1.lean.expected.out
index 5467f0b49..2679a2d88 100644
--- a/tests/lean/pattern_hint1.lean.expected.out
+++ b/tests/lean/pattern_hint1.lean.expected.out
@@ -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}
diff --git a/tests/lean/redundant_pattern.lean.expected.out b/tests/lean/redundant_pattern.lean.expected.out
index 3ca6801de..535233e15 100644
--- a/tests/lean/redundant_pattern.lean.expected.out
+++ b/tests/lean/redundant_pattern.lean.expected.out
@@ -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)}