max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-12 12:59:08 -07:00
parent a7d08d2f3d
commit e41a2ef3d8
3 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/check.lean.expected.out
View file

@ -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

2
tests/lean/lisp.lean.expected.out
View file

@ -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 "(" [] ")")

14
tests/lean/trust0/basic.lean
View file

@ -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