From c09bb3cc6f2912e0f2044664230a2a318ed680ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 15:34:44 -0700 Subject: [PATCH] fix(tests/lean/notation): remove 'sorry' warning from expected outputs --- tests/lean/notation2.lean.expected.out | 1 - tests/lean/notation3.lean.expected.out | 1 - tests/lean/notation4.lean.expected.out | 1 - 3 files changed, 3 deletions(-) diff --git a/tests/lean/notation2.lean.expected.out b/tests/lean/notation2.lean.expected.out index 87bbe382a5..d2f39b6311 100644 --- a/tests/lean/notation2.lean.expected.out +++ b/tests/lean/notation2.lean.expected.out @@ -1,3 +1,2 @@ -notation2.lean:2:0: warning: imported file uses 'sorry' 1 :: 2 :: nil : list num 1 :: 2 :: 3 :: 4 :: 5 :: nil : list num diff --git a/tests/lean/notation3.lean.expected.out b/tests/lean/notation3.lean.expected.out index 23662a4fc7..66caff64b7 100644 --- a/tests/lean/notation3.lean.expected.out +++ b/tests/lean/notation3.lean.expected.out @@ -1,4 +1,3 @@ -notation3.lean:2:0: warning: imported file uses 'sorry' [ a, b, b ] : list num (a, true, a = b, b) : num × Prop × Prop × num (a, b) : num × num diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out index 33ced86456..d5a812e952 100644 --- a/tests/lean/notation4.lean.expected.out +++ b/tests/lean/notation4.lean.expected.out @@ -1,4 +1,3 @@ -notation4.lean:2:0: warning: imported file uses 'sorry' ∃ (A : Type₁) (x y : A), x = y : Prop ∃ (x : num), x = 0 : Prop Σ (x : num), x = 10 : Type₁