From e41a2ef3d8f167e31b360e4580b5ebc753da1994 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Jun 2018 12:59:08 -0700 Subject: [PATCH] chore(tests/lean): fix tests --- tests/lean/check.lean.expected.out | 2 +- tests/lean/lisp.lean.expected.out | 2 +- tests/lean/trust0/basic.lean | 14 +++++++++++--- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/tests/lean/check.lean.expected.out b/tests/lean/check.lean.expected.out index 1fc5b28442..dc36037239 100644 --- a/tests/lean/check.lean.expected.out +++ b/tests/lean/check.lean.expected.out @@ -1,4 +1,4 @@ and.intro : ?M_1 → ?M_2 → ?M_1 ∧ ?M_2 or.elim : ?M_1 ∨ ?M_2 → (?M_1 → ?M_3) → (?M_2 → ?M_3) → ?M_3 eq : ?M_1 → ?M_1 → Prop -eq.rec : ?M_3 ?M_2 → Π {a : ?M_1}, ?M_2 = a → ?M_3 a +eq.rec : ?M_3 ?M_2 _ → Π {a : ?M_1} (n : ?M_2 = a), ?M_3 a n diff --git a/tests/lean/lisp.lean.expected.out b/tests/lean/lisp.lean.expected.out index 5c002b0c8e..ba3a690d09 100644 --- a/tests/lean/lisp.lean.expected.out +++ b/tests/lean/lisp.lean.expected.out @@ -1,4 +1,4 @@ -lisp.lean:198:0: error: cannot evaluate (list "(" [] ")") +lisp.lean:200:0: error: cannot evaluate (list "(" [] ")") reader: (list "(" [] ")") expander: (list "(" [] ")") resolver: (list "(" [] ")") diff --git a/tests/lean/trust0/basic.lean b/tests/lean/trust0/basic.lean index 37d4772e95..33e9d63cda 100644 --- a/tests/lean/trust0/basic.lean +++ b/tests/lean/trust0/basic.lean @@ -14,6 +14,14 @@ inductive less_than_or_equal (a : ℕ) : ℕ → Prop | refl : less_than_or_equal a | step : Π {b}, less_than_or_equal b → less_than_or_equal (succ b) +@[elab_as_eliminator] +theorem less_than_or_equal.ndrec {a : nat} {C : nat → Prop} (m₁ : C a) (m₂ : ∀ (b : nat), less_than_or_equal a b → C b → C (succ b)) {b : ℕ} (h : less_than_or_equal a b) : C b := +@less_than_or_equal.rec a (λ b _, C b) m₁ m₂ b h + +@[elab_as_eliminator] +theorem less_than_or_equal.ndrec_on {a : nat} {C : nat → Prop} {b : ℕ} (h : less_than_or_equal a b) (m₁ : C a) (m₂ : ∀ (b : nat), less_than_or_equal a b → C b → C (succ b)) : C b := +@less_than_or_equal.rec a (λ b _, C b) m₁ m₂ b h + instance : has_le ℕ := ⟨nat.less_than_or_equal⟩ @@ -66,7 +74,7 @@ lemma le_succ (n : ℕ) : n ≤ succ n := less_than_or_equal.step (nat.le_refl n) lemma succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m := -λ h, less_than_or_equal.rec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h +λ h, less_than_or_equal.ndrec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h lemma zero_le : ∀ (n : ℕ), 0 ≤ n | 0 := nat.le_refl 0 @@ -83,7 +91,7 @@ lemma not_succ_le_zero : ∀ (n : ℕ), succ n ≤ 0 → false lemma not_lt_zero (a : ℕ) : ¬ a < 0 := not_succ_le_zero a lemma pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m := -λ h, less_than_or_equal.rec_on h +λ h, less_than_or_equal.ndrec_on h (nat.le_refl (pred n)) (λ n, nat.rec (λ a b, b) (λ a b c, less_than_or_equal.step) n) @@ -119,7 +127,7 @@ protected lemma lt_irrefl (n : ℕ) : ¬n < n := not_succ_le_self n protected lemma le_trans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k := -less_than_or_equal.rec h1 (λ p h2, less_than_or_equal.step) +less_than_or_equal.ndrec h1 (λ p h2, less_than_or_equal.step) lemma pred_le : ∀ (n : ℕ), pred n ≤ n | 0 := less_than_or_equal.refl 0