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

chore: fix tests

Browse source 
close #402
This commit is contained in:
Leonardo de Moura 2021-08-07 13:22:58 -07:00
parent 9cc94296e5
commit 1d9d8c7e75
27 changed files with 98 additions and 99 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
tests/lean/inductionErrors.lean
View file

@ -10,13 +10,13 @@ theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by
cases p, q using elimEx with
| lower d => apply Or.inl -- Error
| upper d => apply Or.inr -- Error
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl
theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by
cases p, q using elimEx2 with -- Error
| lower d => apply Or.inl
| upper d => apply Or.inr
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl
theorem ex3 (p q : Nat) : p ≤ q ∨ p > q := by
cases p /- Error -/ using elimEx with
@ -28,7 +28,7 @@ theorem ex4 (p q : Nat) : p ≤ q ∨ p > q := by
cases p using Nat.add with -- Error
| lower d => apply Or.inl
| upper d => apply Or.inr
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl
theorem ex5 (x : Nat) : 0 + x = x := by
match x with
@ -58,19 +58,19 @@ theorem ex8 (p q : Nat) : p ≤ q ∨ p > q := by
cases p, q using elimEx with
| lower d => apply Or.inl; admit
| upper2 /- Error -/ d => apply Or.inr
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl
theorem ex9 (p q : Nat) : p ≤ q ∨ p > q := by
cases p, q using elimEx with
| lower d => apply Or.inl; admit
| _ => apply Or.inr; admit
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl
theorem ex10 (p q : Nat) : p ≤ q ∨ p > q := by
cases p, q using elimEx with
| lower d => apply Or.inl; admit
| upper d => apply Or.inr; admit
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl
| _ /- error unused -/ => admit
theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by
@ -78,4 +78,4 @@ theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by
| lower d => apply Or.inl; admit
| upper d => apply Or.inr; admit
| lower d /- error unused -/ => apply Or.inl; admit
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl

4
tests/lean/infoTree.lean.expected.out
View file

@ -75,9 +75,9 @@
x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent
x : Nat @ ⟨17, 43⟩-⟨17, 44⟩
fun x y b =>
ofEqTrue
of_eq_true
(Eq.trans (congrFun (β := fun a => Prop) (f := Eq (x + 0)) (g := Eq x) (congrArg Eq (Nat.add_zero _)) _)
(eqSelf x)) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨18, 2⟩-⟨19, 8⟩ @ Lean.Elab.Term.elabFun
(eq_self x)) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨18, 2⟩-⟨19, 8⟩ @ Lean.Elab.Term.elabFun
Nat : Type @ ⟨18, 6⟩†-⟨18, 7⟩† @ Lean.Elab.Term.elabHole
x : Nat @ ⟨18, 6⟩-⟨18, 7⟩
Nat : Type @ ⟨18, 8⟩†-⟨18, 9⟩† @ Lean.Elab.Term.elabHole

18
tests/lean/interactive/plainTermGoal.lean
View file

@ -1,11 +1,11 @@
--
example : 0 < 2 :=
Nat.ltTrans Nat.zeroLtOne (Nat.ltSuccSelf _)
--^ $/lean/plainTermGoal
Nat.lt_trans Nat.zero_lt_one (Nat.lt_succ_self _)
--^ $/lean/plainTermGoal
--^ $/lean/plainTermGoal
--^ $/lean/plainTermGoal
--^ $/lean/plainTermGoal
--^ $/lean/plainTermGoal
--^ $/lean/plainTermGoal
--^ $/lean/plainTermGoal
example : OptionM Unit := do
let y : Int ← none
@ -14,14 +14,14 @@ example : OptionM Unit := do
return ()
example (m n : Nat) : m < n :=
Nat.ltTrans _ _
--^ $/lean/plainTermGoal
Nat.lt_trans _ _
--^ $/lean/plainTermGoal
example : True := sorry
--^ $/lean/plainTermGoal
example : ∀ n, n < n + 42 :=
fun n => Nat.ltOfLeOfLt (Nat.leAddRight n 41) (Nat.ltSuccSelf _)
fun n => Nat.lt_of_le_of_lt (Nat.le_add_right n 41) (Nat.lt_succ_self _)
--^ $/lean/plainTermGoal
--^ $/lean/plainTermGoal
@ -29,7 +29,7 @@ example : ∀ n, n < 1 + n := by
intro n
rw [Nat.add_comm]
--^ $/lean/plainTermGoal
exact Nat.ltSuccSelf _
exact Nat.lt_succ_self _
--^ $/lean/plainTermGoal
#check fun (n m : Nat) => m

34
tests/lean/interactive/plainTermGoal.lean.expected.out
View file

@ -1,37 +1,37 @@
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 2, "character": 13}}
{"range":
{"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 46}},
"goal": "⊢ 0 < 2"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 2, "character": 14}}
{"range":
{"start": {"line": 2, "character": 14}, "end": {"line": 2, "character": 27}},
"goal": "⊢ 0 < 1"}
{"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 51}},
"goal": "⊢ 0 < 2"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 2, "character": 15}}
{"range":
{"start": {"line": 2, "character": 14}, "end": {"line": 2, "character": 27}},
{"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}},
"goal": "⊢ 0 < 1"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 2, "character": 29}}
"position": {"line": 2, "character": 16}}
{"range":
{"start": {"line": 2, "character": 29}, "end": {"line": 2, "character": 45}},
{"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}},
"goal": "⊢ 0 < 1"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 2, "character": 31}}
{"range":
{"start": {"line": 2, "character": 31}, "end": {"line": 2, "character": 51}},
"goal": "⊢ 1 < 2"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 2, "character": 44}}
"position": {"line": 2, "character": 48}}
{"range":
{"start": {"line": 2, "character": 44}, "end": {"line": 2, "character": 45}},
"goal": "⊢ Nat"}
{"start": {"line": 2, "character": 32}, "end": {"line": 2, "character": 50}},
"goal": "⊢ 1 < 2"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 11, "character": 10}}
{"range":
{"start": {"line": 11, "character": 10}, "end": {"line": 11, "character": 18}},
"goal": "y : Int\n⊢ OptionM Nat"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 16, "character": 16}}
"position": {"line": 16, "character": 17}}
{"range":
{"start": {"line": 16, "character": 16}, "end": {"line": 16, "character": 17}},
{"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}},
"goal": "m n : Nat\n⊢ ?m m n < n"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 19, "character": 18}}
@ -41,7 +41,7 @@
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 23, "character": 2}}
{"range":
{"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 66}},
{"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 74}},
"goal": "⊢ ∀ (n : Nat), n < n + 42"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 23, "character": 6}}
@ -56,7 +56,7 @@
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 31, "character": 8}}
{"range":
{"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 24}},
{"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 26}},
"goal": "n : Nat\n⊢ n < n + 1"}
{"textDocument": {"uri": "file://plainTermGoal.lean"},
"position": {"line": 34, "character": 14}}

2
tests/lean/modBug.lean
View file

@ -1 +1 @@
theorem proofOfFalse : False := Nat.zeroNeOne (Nat.mod_zero 1)
theorem proofOfFalse : False := Nat.zero_ne_one (Nat.mod_zero 1)

4
tests/lean/modBug.lean.expected.out
View file

@ -1,5 +1,5 @@
modBug.lean:1:32-1:62: error: application type mismatch
Nat.zeroNeOne (Nat.mod_zero _)
modBug.lean:1:32-1:64: error: application type mismatch
Nat.zero_ne_one (Nat.mod_zero _)
argument
Nat.mod_zero _
has type

4
tests/lean/run/394.lean
View file

@ -1,7 +1,7 @@
def casesTFOn {motive : Prop → Sort _} (P) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
λ ht hf => match inst with
| isTrue H => eqTrue H ▸ ht
| isFalse H => eqFalse H ▸ hf
| isTrue H => eq_true H ▸ ht
| isFalse H => eq_false H ▸ hf
example (P) [Decidable P] : ¬¬P → P := by
induction P using casesTFOn

3
tests/lean/run/PPTopDownAnalyze.lean
View file

@ -312,7 +312,6 @@ def typeAs (α : Type u) (a : α) := ()
#testDelabN instInhabitedPUnit
#testDelabN Lean.Syntax.getOptionalIdent?
#testDelabN Lean.Meta.ppExpr
#testDelabN Eq.mprProp
#testDelabN MonadLift.noConfusion
#testDelabN MonadLift.noConfusionType
#testDelabN MonadExcept.noConfusion
@ -327,7 +326,7 @@ def typeAs (α : Type u) (a : α) := ()
-- TODO: for some reason this *only* works when trusting subst
set_option pp.analyze.trustSubst true in
#testDelabN Lean.Simp.and_false
#testDelabN and_false
-- TODO: this one prints out a structure instance with keyword field `end`
set_option pp.structureInstances false in

4
tests/lean/run/bigop.lean
View file

@ -28,11 +28,11 @@ instance : Enumerable Bool :=
partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n)
| 0, h => [⟨0, h⟩]
| i+1, h => ⟨i+1, h⟩ :: finElemsAux n i (Nat.ltOfSuccLt h)
| i+1, h => ⟨i+1, h⟩ :: finElemsAux n i (Nat.lt_of_succ_lt h)
partial def finElems : (n : Nat) → List (Fin n)
| 0 => []
| (n+1) => finElemsAux (n+1) n (Nat.ltSuccSelf n)
| (n+1) => finElemsAux (n+1) n (Nat.lt_succ_self n)
instance {n} : Enumerable (Fin n) :=
{ elems := (finElems n).reverse }

14
tests/lean/run/casesUsing.lean
View file

@ -13,7 +13,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by
cases p, q using elimEx with
| diag => apply Or.inl; apply Nat.leRefl
| diag => apply Or.inl; apply Nat.le_refl
| lower d => apply Or.inl; show p ≤ p + d.succ; admit
| upper d => apply Or.inr; show q + d.succ > q; admit
@ -21,7 +21,7 @@ theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by
cases p, q using elimEx
case lower => admit
case upper => admit
case diag => apply Or.inl; apply Nat.leRefl
case diag => apply Or.inl; apply Nat.le_refl
axiom Nat.parityElim (motive : Nat → Sort u)
(even : (n : Nat) → motive (2*n))
@ -93,10 +93,10 @@ theorem modLt (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
rw [Nat.mod_eq_sub_mod h₁.2]
exact ih h
| base x y h₁ =>
match Iff.mp (Decidable.notAndIffOrNot ..) h₁ with
match Iff.mp (Decidable.not_and_iff_or_not ..) h₁ with
| Or.inl h₁ => contradiction
| Or.inr h₁ =>
have hgt := Nat.gtOfNotLe h₁
have hgt := Nat.gt_of_not_le h₁
have heq := Nat.mod_eq_of_lt hgt
rw [← heq] at hgt
assumption
@ -120,7 +120,7 @@ theorem ex13 (p q : Nat) : p ≤ q ∨ p > q := by
| diag => ?hdiag
| lower d => ?hlower
| upper d => ?hupper
case hdiag => apply Or.inl; apply Nat.leRefl
case hdiag => apply Or.inl; apply Nat.le_refl
case hlower => apply Or.inl; show p ≤ p + d.succ; admit
case hupper => apply Or.inr; show q + d.succ > q; admit
@ -129,7 +129,7 @@ theorem ex14 (p q : Nat) : p ≤ q ∨ p > q := by
| diag => ?hdiag
| lower d => _
| upper d => ?hupper
case hdiag => apply Or.inl; apply Nat.leRefl
case hdiag => apply Or.inl; apply Nat.le_refl
case lower => apply Or.inl; show p ≤ p + d.succ; admit
case hupper => apply Or.inr; show q + d.succ > q; admit
@ -138,7 +138,7 @@ theorem ex15 (p q : Nat) : p ≤ q ∨ p > q := by
| diag => ?hdiag
| lower d => _
| upper d => ?hupper
{ apply Or.inl; apply Nat.leRefl }
{ apply Or.inl; apply Nat.le_refl }
{ apply Or.inr; show q + d.succ > q; admit }
{ apply Or.inl; show p ≤ p + d.succ; admit }

2
tests/lean/run/decClassical.lean
View file

@ -5,7 +5,7 @@ theorem ex : if (fun x => x + 1) = (fun x => x + 2) then False else True := by
intro h
have : 1 = 2 := congrFun h 0
contradiction
rw [ifNeg this]
rw [if_neg this]
exact True.intro
def tst (x : Nat) : Bool :=

4
tests/lean/run/def13.lean
View file

@ -12,8 +12,8 @@ rfl
theorem filter_cons_of_pos {a : α} (as : List α) (h : p a) : filter p (a :: as) = a :: filter p as := by
rw [filter_cons];
rw [ifPos h]
rw [if_pos h]
theorem filter_cons_of_neg {a : α} (as : List α) (h : ¬ p a) : filter p (a :: as) = filter p as := by
rw [filter_cons];
rw [ifNeg h]
rw [if_neg h]

26
tests/lean/run/doNotation3.lean
View file

@ -1,19 +1,19 @@
theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b
| 0, _, h => h
| a+1, b, h =>
have : a < b := Nat.ltTrans (Nat.ltSuccSelf _) h
zeroLtOfLt this
have : a < b := Nat.lt_trans (Nat.lt_succ_self _) h
zero_lt_of_lt this
def fold {m α β} [Monad m] (as : Array α) (b : β) (f : α → β → m β) : m β := do
let rec loop : (i : Nat) → i ≤ as.size → β → m β
| 0, h, b => b
| i+1, h, b => do
have h' : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have : as.size - 1 < as.size := Nat.subLt (zeroLtOfLt h') (by decide)
have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
have h' : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
have : as.size - 1 < as.size := Nat.sub_lt (zero_lt_of_lt h') (by decide)
have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
loop i (Nat.leOfLt h') b
loop as.size (Nat.leRefl _) b
loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
#eval Id.run $ fold #[1, 2, 3, 4] 0 (pure $ · + ·)
@ -25,12 +25,12 @@ let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
match i, h with
| 0, h => return b
| i+1, h =>
have h' : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have : as.size - 1 < as.size := Nat.subLt (zeroLtOfLt h') (by decide)
have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
have h' : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
have : as.size - 1 < as.size := Nat.sub_lt (zero_lt_of_lt h') (by decide)
have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
loop i (Nat.leOfLt h') b
loop as.size (Nat.leRefl _) b
loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
def f (x : Nat) (ref : IO.Ref Nat) : IO Nat := do
let mut x := x

4
tests/lean/run/lean3_zulip_issues_1.lean
View file

@ -29,11 +29,11 @@ def f : wrap → Nat
| _ => 1
example (a : Nat) : True := by
have : ∀ n, n ≥ 0 → a ≤ a := fun _ _ => Nat.leRefl ..
have : ∀ n, n ≥ 0 → a ≤ a := fun _ _ => Nat.le_refl ..
exact True.intro
example (ᾰ : Nat) : True := by
have : ∀ n, n ≥ 0 → ᾰ ≤ ᾰ := fun _ _ => Nat.leRefl ..
have : ∀ n, n ≥ 0 → ᾰ ≤ ᾰ := fun _ _ => Nat.le_refl ..
exact True.intro
inductive Vec.{u} (α : Type u) : Nat → Type u

20
tests/lean/run/matchArrayLit.lean
View file

@ -1,17 +1,17 @@
universe u v
theorem eqLitOfSize0 {α : Type u} (a : Array α) (hsz : a.size = 0) : a = #[] :=
a.toArrayLitEq 0 hsz
a.toArrayLit_eq 0 hsz
theorem eqLitOfSize1 {α : Type u} (a : Array α) (hsz : a.size = 1) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl)] :=
a.toArrayLitEq 1 hsz
theorem eqLitOfSize1 {α : Type u} (a : Array α) (hsz : a.size = 1) : a = #[a.getLit 0 hsz (of_decide_eq_true rfl)] :=
a.toArrayLit_eq 1 hsz
theorem eqLitOfSize2 {α : Type u} (a : Array α) (hsz : a.size = 2) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl)] :=
a.toArrayLitEq 2 hsz
theorem eqLitOfSize2 {α : Type u} (a : Array α) (hsz : a.size = 2) : a = #[a.getLit 0 hsz (of_decide_eq_true rfl), a.getLit 1 hsz (of_decide_eq_true rfl)] :=
a.toArrayLit_eq 2 hsz
theorem eqLitOfSize3 {α : Type u} (a : Array α) (hsz : a.size = 3) :
a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl), a.getLit 2 hsz (ofDecideEqTrue rfl)] :=
a.toArrayLitEq 3 hsz
a = #[a.getLit 0 hsz (of_decide_eq_true rfl), a.getLit 1 hsz (of_decide_eq_true rfl), a.getLit 2 hsz (of_decide_eq_true rfl)] :=
a.toArrayLit_eq 3 hsz
/-
Matcher for the following patterns
@ -28,11 +28,11 @@ def matchArrayLit {α : Type u} (C : Array α → Sort v) (a : Array α)
(h₄ : ∀ a, C a)
: C a :=
if h : a.size = 0 then
@Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ (a.toArrayLitEq 0 h).symm
@Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ (a.toArrayLit_eq 0 h).symm
else if h : a.size = 1 then
@Eq.rec _ _ (fun x _ => C x) (h₂ (a.getLit 0 h (ofDecideEqTrue rfl))) _ (a.toArrayLitEq 1 h).symm
@Eq.rec _ _ (fun x _ => C x) (h₂ (a.getLit 0 h (of_decide_eq_true rfl))) _ (a.toArrayLit_eq 1 h).symm
else if h : a.size = 3 then
@Eq.rec _ _ (fun x _ => C x) (h₃ (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl))) _ (a.toArrayLitEq 3 h).symm
@Eq.rec _ _ (fun x _ => C x) (h₃ (a.getLit 0 h (of_decide_eq_true rfl)) (a.getLit 1 h (of_decide_eq_true rfl)) (a.getLit 2 h (of_decide_eq_true rfl))) _ (a.toArrayLit_eq 3 h).symm
else
h₄ a

6
tests/lean/run/matrix.lean
View file

@ -33,14 +33,14 @@ macro_rules
| `($x[$i, $j]) => `($x $i $j)
def dotProduct [Mul α] [Add α] [Zero α] (u v : Fin m → α) : α :=
loop m (Nat.leRefl ..) Zero.zero
loop m (Nat.le_refl ..) Zero.zero
where
loop (i : Nat) (h : i ≤ m) (acc : α) : α :=
match i, h with
| 0, h => acc
| i+1, h =>
have : i < m := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
loop i (Nat.leOfLt this) (acc + u ⟨i, this⟩ * v ⟨i, this⟩)
have : i < m := Nat.lt_of_lt_of_le (Nat.lt_succ_self _) h
loop i (Nat.le_of_lt this) (acc + u ⟨i, this⟩ * v ⟨i, this⟩)
instance [Zero α] : Zero (Matrix m n α) where
zero _ _ := 0

2
tests/lean/run/newfrontend3.lean
View file

@ -17,7 +17,7 @@ by {
def g (i j k : Nat) (a : Array Nat) (h₁ : i < k) (h₂ : k < j) (h₃ : j < a.size) : Nat :=
let vj := a.get ⟨j, h₃⟩;
let vi := a.get ⟨i, Nat.ltTrans h₁ (Nat.ltTrans h₂ h₃)⟩;
let vi := a.get ⟨i, Nat.lt_trans h₁ (Nat.lt_trans h₂ h₃)⟩;
vi + vj
set_option pp.all true in

2
tests/lean/run/noindexAnnotation.lean
View file

@ -3,7 +3,7 @@ structure Fin2 (n : Nat) :=
(isLt : val < n)
protected def Fin2.ofNat {n : Nat} (a : Nat) : Fin2 (Nat.succ n) :=
⟨a % Nat.succ n, Nat.mod_lt _ (Nat.zeroLtSucc _)⟩
⟨a % Nat.succ n, Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
instance : OfNat (Fin2 (no_index (n+1))) i where
ofNat := Fin2.ofNat i

4
tests/lean/run/reduce1.lean
View file

@ -23,7 +23,7 @@ theorem tst5 : 10000000000000000 < 200000000000000000000 :=
theorem tst6 : 10000000000000000 < 200000000000000000000 :=
let h₁ : 10000000000000000 < 10000000000000010 := by nativeDecide
let h₂ : 10000000000000010 < 200000000000000000000 := by nativeDecide
Nat.ltTrans h₁ h₂
Nat.lt_trans h₁ h₂
theorem tst7 : 10000000000000000 < 200000000000000000000 :=
by decide
@ -31,7 +31,7 @@ theorem tst7 : 10000000000000000 < 200000000000000000000 :=
theorem tst8 : 10000000000000000 < 200000000000000000000 :=
let h₁ : 10000000000000000 < 10000000000000010 := by decide
let h₂ : 10000000000000010 < 200000000000000000000 := by decide
Nat.ltTrans h₁ h₂
Nat.lt_trans h₁ h₂
theorem tst9 : 10000000000000000 < 200000000000000000000 :=
by decide

2
tests/lean/run/reduce3.lean
View file

@ -20,7 +20,7 @@ theorem tst4 : fact 10 = 3628800 :=
rfl
theorem tst5 : 100000000001 < 300000000000 :=
ofDecideEqTrue rfl
of_decide_eq_true rfl
theorem tst6 : "hello".length = 5 :=
rfl

6
tests/lean/run/simp7.lean
View file

@ -10,7 +10,7 @@ def length : List α → Nat
theorem ex2 (a b c : α) (as : List α) : length (a :: b :: as) > length as := by
simp [length]
apply Nat.lt.step
apply Nat.ltSuccSelf
apply Nat.lt_succ_self
def fact : Nat → Nat
| 0 => 1
@ -21,8 +21,8 @@ theorem ex3 : fact x > 0 := by
| zero => rfl
| succ x ih =>
simp [fact]
apply Nat.mulPos
apply Nat.zeroLtSucc
apply Nat.mul_pos
apply Nat.zero_lt_succ
apply ih
def head [Inhabited α] : List α → α

2
tests/lean/run/subst.lean
View file

@ -52,7 +52,7 @@ theorem ex12 {α : Type u} {n : Nat}
Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ hi₂ => h i (hsz₁ ▸ hi₁)
def toArrayLit {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
List.toArray $ Array.toListLitAux a n hsz n (hsz ▸ Nat.leRefl _) []
List.toArray $ Array.toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
partial def isEqvAux {α} (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
if h : i < a.size then

4
tests/lean/run/synthPending1.lean
View file

@ -1,4 +1,4 @@
--
theorem ex : Not (1 = 2) :=
ofDecideEqFalse rfl
of_decide_eq_false rfl

2
tests/lean/run/trans.lean
View file

@ -4,7 +4,7 @@ class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α
export Trans (trans)
instance : Trans (α := Nat) (β := Nat) (γ := Nat) (.≤.) (.≤.) (.≤.) where
trans := Nat.leTrans
trans := Nat.le_trans
instance : Trans (α := Int) (β := Int) (γ := Int) (.≤.) (.≤.) (.≤.) where
trans := sorry

2
tests/lean/simpArgTypeMismatch.lean
View file

@ -1,3 +1,3 @@
example (p : Prop) [Decidable p] (hnp : ¬ p) :
if decide p then 0 = 1 else 1 = 1 := by
simp [hnp, decideEqFalse Unit]
simp [hnp, decide_eq_false Unit]

4
tests/lean/simpArgTypeMismatch.lean.expected.out
View file

@ -1,5 +1,5 @@
simpArgTypeMismatch.lean:3:13-3:31: error: application type mismatch
decideEqFalse Unit
simpArgTypeMismatch.lean:3:13-3:33: error: application type mismatch
decide_eq_false Unit
argument
Unit
has type

4
tests/lean/uintCtors.lean
View file

@ -18,7 +18,7 @@ def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
#eval (3 : UInt32).val
#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt64 }
#eval (3 : UInt64).val
#eval toString $ { val := { val := 3, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
#eval toString $ { val := { val := 3, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
#eval (3 : USize).val
@ -30,5 +30,5 @@ def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
#eval (4 : UInt32).val
#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt64 }
#eval (4 : UInt64).val
#eval toString $ { val := { val := 4, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
#eval toString $ { val := { val := 4, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
#eval (4 : USize).val