chore(tests/lean): make sure tests only use init and systems.IO

tests/lean/559.lean

@@ -1,12 +0,0 @@
-import algebra.ordered_field
-open algebra
-section sequence_c
-
-  parameter Q : Type
-  parameter lof_Q : linear_ordered_field Q
-  definition to_lof [instance] : linear_ordered_field Q := lof_Q
-  include to_lof
-
-  theorem foo (a b : Q) : a + b = b + a := add.comm a b
-
-end sequence_c

tests/lean/559.lean.expected.out

@@ -1,4 +0,0 @@
-559.lean:10:28: error: failed to synthesize placeholder
-Q : Type,
-a b : Q
-⊢ has_add Q

tests/lean/alias.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 namespace N1
   constant num : Type.{1}

tests/lean/alias2.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 namespace foo
    definition t := true

tests/lean/auto_include.lean

@@ -1,32 +0,0 @@
-import algebra.group
-open algebra
-
-section
-variables {A : Type} [group A]
-variables {B : Type} [group B]
-
-definition foo (a b : A) : a * b = b * a :=
-sorry
-
-definition bla (b : B) : b * 1 = b :=
-sorry
-
-print foo
-print bla
-end
-
-section
-variable {A : Type}
-variable [group A]
-variable {B : Type}
-variable [group B]
-
-definition foo2 (a b : A) : a * b = b * a :=
-sorry
-
-definition bla2 (b : B) : b * 1 = b :=
-sorry
-
-print foo2
-print bla2
-end

tests/lean/auto_include.lean.expected.out

@@ -1,8 +0,0 @@
-definition foo : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
-λ A _inst_1 a b, sorry
-definition bla : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
-λ B _inst_2 b, sorry
-definition foo2 : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
-λ A _inst_1 a b, sorry
-definition bla2 : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
-λ B _inst_2 b, sorry

tests/lean/bad_class.lean

@@ -1,4 +1,4 @@
-import logic
+--
 namespace foo
 definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b
 attribute subsingleton [class]

tests/lean/bad_id.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 
 definition x.y : nat := 10
 

tests/lean/bad_notation.lean

@@ -1,4 +1,4 @@
-import logic
+--
 open nat
 
 section

tests/lean/by_contradiction.lean

@@ -1,4 +1,4 @@
-import data.nat
+--
 open tactic nat
 
 example (a b : nat) : a ≠ b → ¬ a = b :=

tests/lean/check.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 check and.intro
 check or.elim

tests/lean/check2.lean

@@ -1,3 +1,3 @@
-import logic
+--
 
 check eq.rec_on

tests/lean/cls_err.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 inductive H [class] (A : Type) :=
 mk : A → H A

tests/lean/congr_print.lean

@@ -1,5 +0,0 @@
-import data.list
-open list perm
-
-set_option pp.max_depth 10
-print perm_erase_dup_of_perm

tests/lean/congr_print.lean.expected.out

@@ -1,2 +0,0 @@
-theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
-λ A H l₁ l₂, sorry

tests/lean/const.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 
 definition foo {A : Type} [H : inhabited A] : A :=

tests/lean/crash.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 section
 hypothesis P : Prop.

tests/lean/ctxopt.lean

@@ -1,4 +1,4 @@
-import logic
+--
 -- definition id {A : Type} (a : A) := a
 
 section

tests/lean/elab10.lean

@@ -1,20 +0,0 @@
-import algebra.ring
-set_option pp.notation false
-set_option pp.implicit true
-set_option pp.numerals false
-set_option pp.binder_types true
-
-check ∀ (A : Type) [has_add A] [has_zero A] [has_lt A] (a : A), a = 0 + 0 → a + a > 0
-
-constant int : Type₁
-constant int_comm_ring : comm_ring int
-attribute int_comm_ring [instance]
-
-check int → int
-
-check ((λ x, x + 1) : int → int)
-
-check λ (A : Type) (a b c d : A) (H1 : a = b) (H2 : b = c) (H3 : d = c),
-     have a = c, from eq.trans H1 H2,
-     have H3' : c = d, from eq.symm H3,
-     show a = d, from eq.trans this H3'

tests/lean/elab10.lean.expected.out

@@ -1,14 +0,0 @@
-∀ (A : Type) [_inst_1 : has_add A] [_inst_2 : has_zero A] [_inst_3 : has_lt A] (a : A),
-  @eq A a (@add A _inst_1 (@zero A _inst_2) (@zero A _inst_2)) →
-  @gt A _inst_3 (@add A _inst_1 a a) (@zero A _inst_2) :
-  Prop
-int → int : Type
-λ (x : int),
-  @add int (@distrib.to_has_add int (@ring.to_distrib int (@comm_ring.to_ring int int_comm_ring))) x
-    (@one int (@monoid.to_has_one int (@ring.to_monoid int (@comm_ring.to_ring int int_comm_ring)))) :
-  int → int
-λ (A : Type) (a b c d : A) (H1 : @eq A a b) (H2 : @eq A b c) (H3 : @eq A d c),
-  have this : @eq A a c, from @eq.trans A a b c H1 H2,
-  have H3' : @eq A c d, from @eq.symm A d c H3,
-  show @eq A a d, from @eq.trans A a c d this H3' :
-  ∀ (A : Type) (a b c d : A), @eq A a b → @eq A b c → @eq A d c → @eq A a d

tests/lean/empty.lean

@@ -1,4 +1,4 @@
-import logic
+--
 open inhabited nonempty classical
 
 noncomputable definition v1 : Prop := epsilon (λ x, true)

tests/lean/error_loc_bug.lean

@@ -1,78 +0,0 @@
-/-
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-
-Define propositional calculus, valuation, provability, validity, prove soundness.
-
-This file is based on Floris van Doorn Coq files.
-
-Similar to soundness.lean, but defines Nc in Type.
-The idea is to be able to prove soundness using recursive equations.
--/
-import data.nat data.list
-open nat bool list decidable
-
-definition PropVar [reducible] := nat
-
-inductive PropF :=
-| Var  : PropVar → PropF
-| Bot  : PropF
-| Conj : PropF → PropF → PropF
-| Disj : PropF → PropF → PropF
-| Impl : PropF → PropF → PropF
-
-namespace PropF
-  notation `#`:max P:max := Var P
-  local notation A ∨ B   := Disj A B
-  local notation A ∧ B   := Conj A B
-  infixr `⇒`:27          := Impl
-  notation `⊥`           := Bot
-
-  definition Neg A       := A ⇒ ⊥
-  notation ~ A           := Neg A
-  definition Top         := ~⊥
-  notation `⊤`           := Top
-  definition BiImpl A B  := A ⇒ B ∧ B ⇒ A
-  infixr `⇔`:27          := BiImpl
-
-  definition valuation   := PropVar → bool
-
-  reserve infix ` ⊢ `:26
-
-  /- Provability -/
-
-  inductive Nc : list PropF → PropF → Type :=
-  infix ⊢ := Nc
-  | Nax   : ∀ Γ A,   A ∈ Γ →             Γ ⊢ A
-  | ImpI  : ∀ Γ A B, A::Γ ⊢ B →          Γ ⊢ A ⇒ B
-  | ImpE  : ∀ Γ A B, Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
-  | BotC  : ∀ Γ A,   (~A)::Γ ⊢ ⊥ →       Γ ⊢ A
-  | AndI  : ∀ Γ A B, Γ ⊢ A → Γ ⊢ B →     Γ ⊢ A ∧ B
-  | AndE₁ : ∀ Γ A B, Γ ⊢ A ∧ B →         Γ ⊢ A
-  | AndE₂ : ∀ Γ A B, Γ ⊢ A ∧ B →         Γ ⊢ B
-  | OrI₁  : ∀ Γ A B, Γ ⊢ A →             Γ ⊢ A ∨ B
-  | OrI₂  : ∀ Γ A B, Γ ⊢ B →             Γ ⊢ A ∨ B
-  | OrE   : ∀ Γ A B C, Γ ⊢ A ∨ B → A::Γ ⊢ C → B::Γ ⊢ C → Γ ⊢ C
-
-  infix ⊢ := Nc
-  open Nc
-
-  -- Remark ⌞t⌟ indicates we should not pattern match on t.
-  -- In the following lemma, we only need to pattern match on Γ ⊢ A,
-
-  lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
-  | Γ A       Δ (Nax Γ A Hin)          Hs := Nax _ _ (Hs A Hin)
-  | Γ (A ⇒ B) Δ (ImpI Γ A B H)         Hs := ImpI _ _ _ (weakening2 H (cons_sub_cons A Hs))
-  | Γ B       Δ (ImpE Γ A B H₁ H₂)     Hs := ImpE _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
-  | Γ A       Δ (BotC Γ A H)           Hs := BotC _ _ (weakening2 H (cons_sub_cons (~A) Hs))
-  | Γ (A ∧ B) Δ (AndI Γ A B H₁ H₂)     Hs := AndI _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
-  | Γ A       Δ (AndE₁ Γ A B H)        Hs := AndE₁ _ _ _ (weakening2 H Hs)
-  | Γ B       Δ (AndE₂ Γ A B H)        Hs := AndE₂ _ _ _ (weakening2 H Hs)
-  | Γ (A ∧ B) Δ (OrI₁ Γ A B H)         Hs := OrI₁ _ _ _ (weakening2 H Hs)
-  | Γ (A ∨ B) Δ (OrI₂ Γ A B H)         Hs := OrI₂ _ _ _ (weakening2 H Hs)
-  | Γ C       Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
-       OrE _ _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ (cons_sub_cons A Hs)) (weakening2 H₃ (cons_sub_cons B Hs))
-
-end PropF

tests/lean/error_loc_bug.lean.expected.out

@@ -1,8 +0,0 @@
-error_loc_bug.lean:73:17: error: type mismatch at application
-  weakening2 (OrI₁ Γ A B H)
-term
-  OrI₁ Γ A B H
-has type
-  Γ ⊢ A ∨ B
-but is expected to have type
-  Γ ⊢ A ∧ B

tests/lean/eta_bug.lean

@@ -1,4 +1,4 @@
-import logic
+--
 eval λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
 -- Should not reduce to
 -- λ (A : Type) (x y : A), eq.trans

tests/lean/export1.lean

@@ -1,38 +0,0 @@
-import data.nat
-
-namespace foo
-  export nat
-  check gcd
-end foo
-
-check gcd
-
-namespace foo
-  check gcd
-end foo
-
-check gcd
-
-namespace bla
-   check gcd
-   export foo
-   check gcd
-end bla
-
-section
-  open bla
-  check gcd
-end
-
-check gcd
-
-section
-  open foo
-  check gcd
-end
-
-check gcd
-
-open bla foo nat
-print raw gcd
-check gcd

tests/lean/export1.lean.expected.out

@@ -1,12 +0,0 @@
-gcd : ℕ → ℕ → ℕ
-export1.lean:8:6: error: unknown identifier 'gcd'
-gcd : ℕ → ℕ → ℕ
-export1.lean:14:6: error: unknown identifier 'gcd'
-export1.lean:17:9: error: unknown identifier 'gcd'
-gcd : ℕ → ℕ → ℕ
-gcd : ℕ → ℕ → ℕ
-export1.lean:27:6: error: unknown identifier 'gcd'
-gcd : ℕ → ℕ → ℕ
-export1.lean:34:6: error: unknown identifier 'gcd'
-gcd
-gcd : ℕ → ℕ → ℕ

tests/lean/have1.lean

@@ -1,14 +0,0 @@
-import logic
-open bool tactic eq
-notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
-notation H1 ⬝ H2 := trans H1 H2
-constants a b c : bool
-axiom H1 : a = b
-axiom H2 : b = c
-check have e1 : a = b, from H1,
-      have e2 : a = c, from sorry, -- by apply trans; apply e1; apply H2,
-      have e3 : c = a, from e2⁻¹,
-      have e4 : b = a, from e1⁻¹,
-      have e5 : b = c, from e4 ⬝ e2,
-      have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹,
-      e3 ⬝ e2

tests/lean/have1.lean.expected.out

@@ -1,8 +0,0 @@
-have e1 : a = b, from H1,
-have e2 : a = c, from sorry,
-have e3 : c = a, from e2⁻¹,
-have e4 : b = a, from e1⁻¹,
-have e5 : b = c, from e4 ⬝ e2,
-have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹,
-e3 ⬝ e2 :
-  c = c

tests/lean/ind_parser_bug.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 inductive acc1 (A : Type) (R : A → A → Prop) (a : A) :  Prop :=
 intro : ∀ (x : A), (∀ (y : A), R y x → acc1 A R y) → acc1 A R x

tests/lean/inst.lean

@@ -1,4 +1,4 @@
-import logic data.prod
+--
 set_option pp.notation false
 
 inductive C [class] (A : Type) :=

tests/lean/let3.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 
 
 constant f : num → num → num → num

tests/lean/let4.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 
 
 constant f : num → num → num → num

tests/lean/nested1.lean

@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat
 
 namespace test

tests/lean/no_confusion_type.lean

@@ -1,4 +1,4 @@
-import logic
+--
 open nat
 
 inductive vector (A : Type) : nat → Type :=

tests/lean/notation.lean

@@ -1,4 +1,4 @@
-import logic data.num
+--
 open num
 constant b : num
 check b + b + b

tests/lean/notation2.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 inductive List (T : Type) : Type := nil {} : List T | cons   : T → List T → List T open List notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 infixr `::` := cons
 check (1:num) :: 2 :: nil

tests/lean/notation3.lean

@@ -1,4 +1,4 @@
-import data.prod data.num
+--
 inductive List (T : Type) : Type := nil {} : List T | cons   : T → List T → List T open List notation h :: t  := cons h t notation `[` l:(foldr `, ` (h t, cons h t) nil) `]` := l
 open prod num
 constants a b : num

tests/lean/notation4.lean

@@ -1,4 +1,4 @@
-import logic data.sigma
+--
 open sigma
 inductive List (T : Type) : Type := nil {} : List T | cons   : T → List T → List T open List notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 check ∃ (A : Type₁) (x y : A), x = y

tests/lean/notation5.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 
 notation `((` := 1
 

tests/lean/notation6.lean

@@ -1,4 +1,4 @@
-import logic data.num
+--
 open num
 notation `o` := (10:num)
 check 11

tests/lean/notation7.lean

@@ -1,4 +1,4 @@
-import logic data.num
+--
 open num
 
 constant f : num → num

tests/lean/num.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 
 
 check 10

tests/lean/num3.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 set_option pp.notation false
 set_option pp.implicit true
 

tests/lean/num4.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 set_option pp.notation false
 set_option pp.implicit true
 

tests/lean/num5.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 open num
 
 eval 3+(2:num)

tests/lean/param.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 open num
 
 definition foo1 a b c := a + b + (c:num)

tests/lean/parsing_only.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 constant f : num → num
 constant g : num → num

tests/lean/pp_algebra_num_bug.lean

@@ -1,19 +0,0 @@
-import algebra.group
-open algebra
-
-variable {A : Type}
-variable [s : group A]
-variable (a : A)
-
-check 1 * 1 * a
-set_option pp.notation false
-check 1 * a
-
-variable [s2 : add_comm_group A]
-
-set_option pp.notation true
-
-check 0 + a
-
-set_option pp.notation false
-check 0 + a

tests/lean/pp_algebra_num_bug.lean.expected.out

@@ -1,4 +0,0 @@
-1 * 1 * a : A
-mul 1 a : A
-0 + a : A
-add 0 a : A

tests/lean/pp_all.lean

@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat
 
 variables {a : nat}

tests/lean/pp_all2.lean

@@ -1,4 +1,4 @@
-import data.nat
+--
 
 set_option pp.all       true
 set_option pp.numerals  true

tests/lean/pp_no_proofs.lean

@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat
 
 constants (P : ∀ {t:true}, ℕ → Prop) (P0 : @P trivial 0)

tests/lean/protected.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 namespace foo
   protected definition C := true

tests/lean/record_rec_protected.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 structure point (A : Type) (B : Type) :=
 mk :: (x : A) (y : B)

tests/lean/reserve_bugs.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 constant f : num → num
 constant g : num → num → num

tests/lean/rewrite1.lean

@@ -1,48 +0,0 @@
-import data.nat
-open nat tactic
-
-example (a b : nat) : a * 0 + 0 + b + 0 = b :=
-by do
- rewrite `mul_zero,
- trace_state,
- rewrite `add_zero,
- repeat $ rewrite `zero_add
-
-print "---------"
-
-example (a b : nat) (H : a + b * 0 + 0 = b) : b = a :=
-by do
- rewrite_at `mul_zero `H,
- trace_state,
- rewrite_at `add_zero `H,
- rewrite_at `add_zero `H,
- symmetry,
- assumption
-
-print "---------"
-
-example (a : nat) : (0 + a) + (0 + a) + (0 + a) = a + a + a :=
-by rewrite `zero_add
-
-meta_definition rewrite_occs (th_name : name) (occs : list nat) : tactic unit :=
-do th ← mk_const th_name,
-   rewrite_core reducible tt (occurrences.pos occs) ff th,
-   try reflexivity
-
-print "---------"
-
-example (a : nat) : (0 + a) + (0 + a) + (0 + a) = a + a + a :=
-by do
-   rewrite_occs `zero_add [1, 3],
-   trace_state,
-   rewrite `zero_add
-
-print "---------"
-
-example (a : nat) : (0 + a) + (0 + a) + (0 + a) = a + a + a :=
-by do
-   rewrite_occs `zero_add [2],
-   trace_state,
-   rewrite_occs `zero_add [2],
-   trace_state,
-   rewrite `zero_add

tests/lean/rewrite1.lean.expected.out

@@ -1,15 +0,0 @@
-a b : ℕ
-⊢ 0 + 0 + b + 0 = b
----------
-a b : ℕ,
-H : a + 0 + 0 = b
-⊢ b = a
----------
----------
-a : ℕ
-⊢ a + (0 + a) + a = a + a + a
----------
-a : ℕ
-⊢ 0 + a + a + (0 + a) = a + a + a
-a : ℕ
-⊢ 0 + a + a + a = a + a + a

tests/lean/rquote.lean

@@ -1,5 +1,5 @@
-import data.nat
-
+--
+constant nat.gcd : nat → nat → nat
 namespace foo
  constant f : nat → nat
  constant g : nat → nat

tests/lean/sec.lean

@@ -1,4 +1,4 @@
-import data.prod
+--
 open prod
 
 section

tests/lean/show1.lean

@@ -1,14 +0,0 @@
-import logic
-open bool eq tactic
-notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
-notation H1 ⬝ H2 := trans H1 H2
-constants a b c : bool
-axiom H1 : a = b
-axiom H2 : b = c
-check show a = c, from H1 ⬝ H2
-print "------------"
-check have e1 : a = b, from H1,
-      have e2 : a = c, from sorry, -- by apply eq.trans; apply e1; apply H2,
-      have e3 : c = a, from e2⁻¹,
-      have e4 : b = a, from e1⁻¹,
-      show b = c, from e1⁻¹ ⬝ e2

tests/lean/show1.lean.expected.out

@@ -1,8 +0,0 @@
-show a = c, from H1 ⬝ H2 : a = c
-------------
-have e1 : a = b, from H1,
-have e2 : a = c, from sorry,
-have e3 : c = a, from e2⁻¹,
-have e4 : b = a, from e1⁻¹,
-show b = c, from e1⁻¹ ⬝ e2 :
-  b = c

tests/lean/subpp.lean

@@ -1,4 +1,4 @@
--- import data.subtype
+--
 open nat subtype
 
 check {x : nat \ x > 0 }

tests/lean/tuple.lean

@@ -1,4 +1,4 @@
-import data.prod
+--
 open nat prod
 
 set_option pp.universes true

tests/lean/unfold2.lean

@@ -1,21 +0,0 @@
-import data.nat
-open nat
-
-definition fact1 : nat → nat
-| 0        := 1
-| (succ a) := (succ a) * fact1 a
-
-open tactic
-
-example (a : nat) : fact1 a > 0 :=
-by do
-  get_local `a >>= λ H, induction_core semireducible H `nat.rec_on [`n, `iH],
-  trace_state, trace "-------",
-  unfold [`fact1],
-  swap,
-  unfold [`fact1],
-  trace_state,
-  mk_const `mul_pos >>= apply,
-  mk_const `nat.zero_lt_succ >>= apply,
-  assumption,
-  mk_const `zero_lt_one >>= apply

tests/lean/unfold2.lean.expected.out

@@ -1,11 +0,0 @@
-⊢ fact1 0 > 0
-
-n : ℕ,
-iH : fact1 n > 0
-⊢ fact1 (succ n) > 0
--------
-n : ℕ,
-iH : fact1 n > 0
-⊢ succ n * fact1 n > 0
-
-⊢ 1 > 0

tests/lean/unfold3.lean

@@ -1,24 +0,0 @@
-import data.nat
-open nat tactic
-
-definition fib : nat → nat
-| 0        := 1
-| 1        := 1
-| (n+2)    := fib n + fib (n+1)
-
-example (a : nat) : fib a > 0 :=
-by do
-  get_local `a >>= λ H, induction_core semireducible H `nat.rec_on [`n, `iH1],
-  trace_state, trace "-------",
-  unfold [`fib],
-  trace_state, trace "-------",
-  mk_const `zero_lt_one >>= apply,
-  trace_state, trace "-------",
-  get_local `n >>= cases,
-  unfold [`fib],
-  mk_const `zero_lt_one >>= apply,
-  unfold [`fib],
-  trace_state,
-  mk_const `add_pos_of_nonneg_of_pos >>= apply,
-  mk_const `nat.zero_le >>= apply,
-  assumption

tests/lean/unfold3.lean.expected.out

@@ -1,19 +0,0 @@
-⊢ fib 0 > 0
-
-n : ℕ,
-iH1 : fib n > 0
-⊢ fib (succ n) > 0
--------
-⊢ 1 > 0
-
-n : ℕ,
-iH1 : fib n > 0
-⊢ fib (succ n) > 0
--------
-n : ℕ,
-iH1 : fib n > 0
-⊢ fib (succ n) > 0
--------
-a : ℕ,
-iH1 : fib (succ a) > 0
-⊢ fib a + fib (succ a) > 0

tests/lean/unfold4.lean

@@ -1,7 +1,7 @@
-import data.nat
-import init.meta.tactic
+--
+--
 open tactic
--- import init.meta.tactics
+--
 
 inductive vector (A : Type) : nat → Type :=
   | nil {} : vector A 0

tests/lean/unfold_crash.lean

@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat tactic
 
 example (a b : nat) : a = succ b → a = b + 1 :=

tests/lean/unfold_crash2.lean

@@ -1,4 +1,4 @@
-import data.nat
+--
 open tactic
 
 inductive vector (A : Type) : nat → Type :=

tests/lean/unfold_fact.lean

@@ -1,24 +0,0 @@
-import data.nat
-open nat
-
-definition fact1 : nat → nat
-| 0        := 1
-| (succ a) := (succ a) * fact1 a
-
-open tactic
-
-example (a : nat) : fact1 a > 0 :=
-by do
-  -- fact1 should not be unfolded since argument is not 0 or succ
-  unfold [`fact1],
-  trace_state, trace "-------",
-  get_local `a >>= λ H, induction_core semireducible H `nat.rec_on [`n, `iH],
-  -- now it should unfold
-  unfold [`fact1],
-  swap,
-  unfold [`fact1],
-  trace_state,
-  mk_const `mul_pos >>= apply,
-  mk_const `nat.zero_lt_succ >>= apply,
-  assumption,
-  mk_const `zero_lt_one >>= apply

tests/lean/unfold_fact.lean.expected.out

@@ -1,8 +0,0 @@
-a : ℕ
-⊢ fact1 a > 0
--------
-n : ℕ,
-iH : fact1 n > 0
-⊢ succ n * fact1 n > 0
-
-⊢ 1 > 0

tests/lean/uni_bug1.lean

@@ -1,4 +1,4 @@
-import data.prod
+--
 open nat prod
 
 constant R : nat → nat → Prop

tests/lean/unification_hints1.lean

@@ -1,4 +1,4 @@
-import data.list data.nat
+--
 open list nat
 
 structure unification_constraint := {A : Type} (lhs : A) (rhs : A)

tests/lean/unifier_bug.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 theorem test {A B : Type} {a : A} {b : B} (H : a == b) :
            eq.rec_on (type_eq_of_heq H) a = b

tests/lean/univ.lean

@@ -1,4 +1,4 @@
-import data.num
+--
 
 definition id2 (A : Type) (a : A) := a
 

tests/lean/univ_vars.lean

@@ -1,4 +1,4 @@
-import logic
+--
 set_option pp.universes true
 
 universe u

tests/lean/var.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 
 section

tests/lean/var2.lean

@@ -1,4 +1,4 @@
-import logic
+--
 
 
 section