From 9fb7aa9f1cce0cb9e3d388828f81b7cd3c4e5ff1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Apr 2015 19:33:21 -0700 Subject: [PATCH] chore(tests): remove most occurrences of 'context' command from the test suite --- tests/lean/cls_err.lean | 2 +- tests/lean/crash.lean | 2 +- tests/lean/ctxopt.lean | 2 +- tests/lean/ctxopt.lean.expected.out | 2 +- tests/lean/fold.lean | 19 +++++++++++-------- tests/lean/hott/360_2.hlean | 2 +- tests/lean/hott/443.hlean | 2 +- tests/lean/hott/443_b.hlean | 2 +- tests/lean/hott/apply_class_issue.hlean | 2 +- tests/lean/hott/bug_struct_level.hlean | 4 ++-- tests/lean/open_tst.lean | 10 +++++----- tests/lean/run/466.lean | 2 +- tests/lean/run/alg_rw.lean | 4 ++-- tests/lean/run/algebra1.lean | 6 +++--- tests/lean/run/alias3.lean | 6 +++--- tests/lean/run/basic.lean | 6 +++--- tests/lean/run/cody1.lean | 4 ++-- tests/lean/run/cody2.lean | 4 ++-- tests/lean/run/def_tac.lean | 2 +- tests/lean/run/eq20.lean | 2 +- tests/lean/run/group.lean | 6 +++--- tests/lean/run/group2.lean | 6 +++--- tests/lean/run/group3.lean | 4 ++-- tests/lean/run/imp3.lean | 2 +- tests/lean/run/indbug2.lean | 2 +- tests/lean/run/localcoe.lean | 2 +- tests/lean/run/match3.lean | 2 +- tests/lean/run/n4.lean | 8 ++++---- tests/lean/run/one.lean | 2 +- tests/lean/run/record2.lean | 4 ++-- tests/lean/run/sec_var.lean | 2 +- tests/lean/run/section3.lean | 2 +- tests/lean/run/section4.lean | 6 +++--- tests/lean/run/simple.lean | 2 +- tests/lean/run/struct_bug1.lean | 2 +- tests/lean/run/structure_test.lean | 2 +- tests/lean/run/t11.lean | 2 +- tests/lean/run/univ1.lean | 2 +- tests/lean/run/univs.lean | 2 +- tests/lean/sec3.lean | 2 +- tests/lean/t14.lean | 14 +++++++------- tests/lean/t3.lean | 8 ++++---- tests/lean/t4.lean | 2 +- tests/lean/t7.lean | 2 +- tests/lean/var.lean | 2 +- tests/lean/var2.lean | 2 +- 46 files changed, 90 insertions(+), 87 deletions(-) diff --git a/tests/lean/cls_err.lean b/tests/lean/cls_err.lean index 7f5b3132d..ca62a559d 100644 --- a/tests/lean/cls_err.lean +++ b/tests/lean/cls_err.lean @@ -6,7 +6,7 @@ mk : A → H A definition foo {A : Type} [h : H A] : A := H.rec (λa, a) h -context +section variable A : Type variable h : H A definition tst : A := diff --git a/tests/lean/crash.lean b/tests/lean/crash.lean index db7e8bd4a..1130a7fe7 100644 --- a/tests/lean/crash.lean +++ b/tests/lean/crash.lean @@ -1,6 +1,6 @@ import logic -context +section hypothesis P : Prop. definition crash diff --git a/tests/lean/ctxopt.lean b/tests/lean/ctxopt.lean index af96a7f26..32ac6b6c6 100644 --- a/tests/lean/ctxopt.lean +++ b/tests/lean/ctxopt.lean @@ -1,7 +1,7 @@ import logic definition id {A : Type} (a : A) := a -context +section set_option pp.implicit true check id true end diff --git a/tests/lean/ctxopt.lean.expected.out b/tests/lean/ctxopt.lean.expected.out index d75e4dd64..2e5262270 100644 --- a/tests/lean/ctxopt.lean.expected.out +++ b/tests/lean/ctxopt.lean.expected.out @@ -1,2 +1,2 @@ @id Prop true : Prop -id true : Prop +@id Prop true : Prop diff --git a/tests/lean/fold.lean b/tests/lean/fold.lean index f29e2ebba..4d88f2ea8 100644 --- a/tests/lean/fold.lean +++ b/tests/lean/fold.lean @@ -3,29 +3,32 @@ definition Prop := Type.{0} inductive true : Prop := intro : true inductive fals inductive prod (A B : Type) := mk : A → B → prod A B infixl `×`:30 := prod variables a b c : num -context - notation `(` t:(foldr `,` (e r, prod.mk e r)) `)` := t +section + local notation `(` t:(foldr `,` (e r, prod.mk e r)) `)` := t check (a, false, b, true, c) set_option pp.notation false check (a, false, b, true, c) end -context - notation `(` t:(foldr `,` (e r, prod.mk r e)) `)` := t +section + local notation `(` t:(foldr `,` (e r, prod.mk r e)) `)` := t + set_option pp.notation true check (a, false, b, true, c) set_option pp.notation false check (a, false, b, true, c) end -context - notation `(` t:(foldl `,` (e r, prod.mk r e)) `)` := t +section + local notation `(` t:(foldl `,` (e r, prod.mk r e)) `)` := t + set_option pp.notation true check (a, false, b, true, c) set_option pp.notation false check (a, false, b, true, c) end -context - notation `(` t:(foldl `,` (e r, prod.mk e r)) `)` := t +section + local notation `(` t:(foldl `,` (e r, prod.mk e r)) `)` := t + set_option pp.notation true check (a, false, b, true, c) set_option pp.notation false check (a, false, b, true, c) diff --git a/tests/lean/hott/360_2.hlean b/tests/lean/hott/360_2.hlean index 1b2f759c1..0669962f7 100644 --- a/tests/lean/hott/360_2.hlean +++ b/tests/lean/hott/360_2.hlean @@ -1,7 +1,7 @@ open is_trunc --structure is_contr [class] (A : Type) : Type -context +section parameters {P : Π(A : Type), A → Type} definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry diff --git a/tests/lean/hott/443.hlean b/tests/lean/hott/443.hlean index 61b0a2895..8ad62b67c 100644 --- a/tests/lean/hott/443.hlean +++ b/tests/lean/hott/443.hlean @@ -2,7 +2,7 @@ import algebra.group algebra.precategory.basic open eq sigma unit category path_algebra -context +section parameters {P₀ : Type} [P : precategory P₀] structure my_structure := (a : P₀) (b : P₀) (f : @hom P₀ P a b) diff --git a/tests/lean/hott/443_b.hlean b/tests/lean/hott/443_b.hlean index f7da25604..d78102bde 100644 --- a/tests/lean/hott/443_b.hlean +++ b/tests/lean/hott/443_b.hlean @@ -5,7 +5,7 @@ open eq sigma unit category path_algebra equiv set_option pp.implicit true set_option pp.universes true set_option pp.notation false -context +section parameters {D₀ : Type} [C : precategory D₀] {D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type} diff --git a/tests/lean/hott/apply_class_issue.hlean b/tests/lean/hott/apply_class_issue.hlean index 1824583c3..db6a6a09d 100644 --- a/tests/lean/hott/apply_class_issue.hlean +++ b/tests/lean/hott/apply_class_issue.hlean @@ -1,6 +1,6 @@ open is_trunc -context +section parameters {P : Π(A : Type), A → Type} definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry diff --git a/tests/lean/hott/bug_struct_level.hlean b/tests/lean/hott/bug_struct_level.hlean index a6005466d..3cf440d69 100644 --- a/tests/lean/hott/bug_struct_level.hlean +++ b/tests/lean/hott/bug_struct_level.hlean @@ -2,7 +2,7 @@ import algebra.precategory.basic open category -context +section parameter {D₀ : Type} parameter (C : precategory D₀) parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type) @@ -22,7 +22,7 @@ context (ID₁ : ID₁_type) end -context +section parameter {D₀ : Type} parameter [C : precategory D₀] parameter {D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type} diff --git a/tests/lean/open_tst.lean b/tests/lean/open_tst.lean index bcf4f8ab6..548c8deb3 100644 --- a/tests/lean/open_tst.lean +++ b/tests/lean/open_tst.lean @@ -1,10 +1,10 @@ -context +section open [notations] [coercions] nat check 1 + 2 check add -- Error aliases were not created end -context +section open [declarations] [notations] nat variable a : nat check a + a @@ -12,7 +12,7 @@ context check a + 1 -- Error coercion from num to nat was not loaded end -context +section open - [classes] nat variable a : nat check a + a @@ -22,7 +22,7 @@ context _ -- Error inhabited instances was not loaded end -context +section open - [classes] [decls] nat variable a : nat check a + a @@ -32,7 +32,7 @@ context _ -- Error inhabited instances was not loaded end -context +section open [classes] nat definition foo3 : inhabited nat := _ diff --git a/tests/lean/run/466.lean b/tests/lean/run/466.lean index 4f8f75463..6716d61fc 100644 --- a/tests/lean/run/466.lean +++ b/tests/lean/run/466.lean @@ -1,6 +1,6 @@ open eq -context +section parameter (A : Type) definition foo (a : A) : a = a := refl a diff --git a/tests/lean/run/alg_rw.lean b/tests/lean/run/alg_rw.lean index acb775d63..d911b3e61 100644 --- a/tests/lean/run/alg_rw.lean +++ b/tests/lean/run/alg_rw.lean @@ -1,7 +1,7 @@ import algebra.group open algebra -context +section variable {A : Type} variable [s : comm_monoid A] include s @@ -13,7 +13,7 @@ end definition one [reducible] (A : Type) [s : has_one A] : A := !has_one.one -context +section variable {A : Type} variable [s : comm_group A] include s diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean index 0ecdef98a..c26351671 100644 --- a/tests/lean/run/algebra1.lean +++ b/tests/lean/run/algebra1.lean @@ -3,13 +3,13 @@ import logic namespace experiment definition Type1 := Type.{1} -context +section variable {A : Type} variable f : A → A → A variable one : A variable inv : A → A - infixl `*` := f - postfix `^-1`:100 := inv + local infixl `*` := f + local postfix `^-1`:100 := inv definition is_assoc := ∀ a b c, (a*b)*c = a*b*c definition is_id := ∀ a, a*one = a definition is_inv := ∀ a, a*a^-1 = one diff --git a/tests/lean/run/alias3.lean b/tests/lean/run/alias3.lean index b5e7f914b..e1e4b495c 100644 --- a/tests/lean/run/alias3.lean +++ b/tests/lean/run/alias3.lean @@ -1,8 +1,8 @@ import logic namespace N1 - context - context + section + section parameter A : Type definition foo (a : A) : Prop := true check foo @@ -14,7 +14,7 @@ end N1 check N1.foo namespace N2 - context + section parameter A : Type inductive list : Type := | nil {} : list diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean index f54dfcb7d..ead66d56a 100644 --- a/tests/lean/run/basic.lean +++ b/tests/lean/run/basic.lean @@ -37,9 +37,9 @@ infix `=`:50 := eq check eq.{1} -context - universe l - universe u +section + universe variable l + universe variable u variable {T1 : Type.{l}} variable {T2 : Type.{l}} variable {T3 : Type.{u}} diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean index 7e4c3d136..98d09f0f8 100644 --- a/tests/lean/run/cody1.lean +++ b/tests/lean/run/cody1.lean @@ -2,7 +2,7 @@ import logic definition subsets (P : Type) := P → Prop. -context +section hypothesis A : Type. @@ -14,7 +14,7 @@ hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a. definition delta (a:A) : Prop := ¬ (r a a). -notation `δ` := delta. +local notation `δ` := delta. -- Crashes unifier! theorem false_aux : ¬ (δ (i delta)) diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean index d18ac0c84..86cb26269 100644 --- a/tests/lean/run/cody2.lean +++ b/tests/lean/run/cody2.lean @@ -2,7 +2,7 @@ import logic open eq definition subsets (P : Type) := P → Prop. -context +section hypothesis A : Type. @@ -14,7 +14,7 @@ hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a. definition delta (a:A) : Prop := ¬ (r a a). -notation `δ` := delta. +local notation `δ` := delta. theorem delta_aux : ¬ (δ (i delta)) := assume H : δ (i delta), diff --git a/tests/lean/run/def_tac.lean b/tests/lean/run/def_tac.lean index 2f4f7ec82..360d31d70 100644 --- a/tests/lean/run/def_tac.lean +++ b/tests/lean/run/def_tac.lean @@ -1,4 +1,4 @@ -context +section open tactic definition cases_refl (e : expr) : tactic := cases e expr_list.nil; apply rfl diff --git a/tests/lean/run/eq20.lean b/tests/lean/run/eq20.lean index a953a9d98..390eff227 100644 --- a/tests/lean/run/eq20.lean +++ b/tests/lean/run/eq20.lean @@ -1,7 +1,7 @@ import data.list open nat list -context +section parameter {A : Type} parameter (p : A → Prop) parameter [H : decidable_pred p] diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index 3c4dc3b9f..02323593b 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -1,12 +1,12 @@ import logic -context +section variable {A : Type} variable f : A → A → A variable one : A variable inv : A → A - infixl `*` := f - postfix `^-1`:100 := inv + local infixl `*` := f + local postfix `^-1`:100 := inv definition is_assoc := ∀ a b c, (a*b)*c = a*b*c definition is_id := ∀ a, a*one = a definition is_inv := ∀ a, a*a^-1 = one diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean index f7ff60a4e..a609eeb8a 100644 --- a/tests/lean/run/group2.lean +++ b/tests/lean/run/group2.lean @@ -1,12 +1,12 @@ import logic -context +section variable {A : Type} variable f : A → A → A variable one : A variable inv : A → A - infixl `*` := f - postfix `^-1`:100 := inv + local infixl `*` := f + local postfix `^-1`:100 := inv definition is_assoc := ∀ a b c, (a*b)*c = a*b*c definition is_id := ∀ a, a*one = a definition is_inv := ∀ a, a*a^-1 = one diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean index ada7477fd..d8c3828aa 100644 --- a/tests/lean/run/group3.lean +++ b/tests/lean/run/group3.lean @@ -43,7 +43,7 @@ section variables {A : Type} [s : semigroup A] variables a b c : A definition mul := semigroup.rec (λmul assoc, mul) s a b - context + section infixl `*` := mul definition assoc : (a * b) * c = a * (b * c) := semigroup.rec (λmul assoc, assoc) s a b c @@ -111,7 +111,7 @@ namespace monoid variables {A : Type} [s : monoid A] variables a b c : A include s - context + section definition mul := monoid.rec (λmul one assoc right_id left_id, mul) s a b definition one := monoid.rec (λmul one assoc right_id left_id, one) s infixl `*` := mul diff --git a/tests/lean/run/imp3.lean b/tests/lean/run/imp3.lean index 9fc586ce9..b82d21cf3 100644 --- a/tests/lean/run/imp3.lean +++ b/tests/lean/run/imp3.lean @@ -3,7 +3,7 @@ structure is_equiv [class] {A B : Type} (f : A → B) := check @is_equiv.inv namespace is_equiv -context +section parameters A B : Type parameter f : A → B parameter c : is_equiv f diff --git a/tests/lean/run/indbug2.lean b/tests/lean/run/indbug2.lean index 1dce9422f..3ba77c9b1 100644 --- a/tests/lean/run/indbug2.lean +++ b/tests/lean/run/indbug2.lean @@ -1,6 +1,6 @@ set_option pp.implicit true set_option pp.universes true -context +section parameter {A : Type} definition foo : A → A → Type := (λ x y, Type) inductive bar {a b : A} (f : foo a b) := diff --git a/tests/lean/run/localcoe.lean b/tests/lean/run/localcoe.lean index 9866919c1..e8f8a7514 100644 --- a/tests/lean/run/localcoe.lean +++ b/tests/lean/run/localcoe.lean @@ -1,6 +1,6 @@ open nat -context +section inductive NatA := | a : NatA | s : NatA → NatA diff --git a/tests/lean/run/match3.lean b/tests/lean/run/match3.lean index 1f903778e..c94bcc047 100644 --- a/tests/lean/run/match3.lean +++ b/tests/lean/run/match3.lean @@ -21,7 +21,7 @@ protected theorem dec_eq : ∀ x y : nat, decidable (x = y) | inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H)) end -context +section open list parameter {A : Type} parameter (p : A → Prop) diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean index 3ed24fafa..6e2e9fb04 100644 --- a/tests/lean/run/n4.lean +++ b/tests/lean/run/n4.lean @@ -1,16 +1,16 @@ prelude definition Prop : Type.{1} := Type.{0} -context +section variable N : Type.{1} variables a b c : N variable and : Prop → Prop → Prop - infixr `∧`:35 := and + local infixr `∧`:35 := and variable le : N → N → Prop variable lt : N → N → Prop precedence `≤`:50 precedence `<`:50 - infixl ≤ := le - infixl < := lt + local infixl ≤ := le + local infixl < := lt check a ≤ b definition T : Prop := a ≤ b check T diff --git a/tests/lean/run/one.lean b/tests/lean/run/one.lean index fbc8a71ca..177d9dc3c 100644 --- a/tests/lean/run/one.lean +++ b/tests/lean/run/one.lean @@ -10,7 +10,7 @@ unit : one2 check one2 -context foo +section foo universe l2 parameter A : Type.{l2} diff --git a/tests/lean/run/record2.lean b/tests/lean/run/record2.lean index 7636e65f6..34a47978d 100644 --- a/tests/lean/run/record2.lean +++ b/tests/lean/run/record2.lean @@ -2,10 +2,10 @@ import logic data.unit set_option pp.universes true -context +section parameter (A : Type) - context + section parameter (B : Type) structure point := diff --git a/tests/lean/run/sec_var.lean b/tests/lean/run/sec_var.lean index a6a042064..a004a59ff 100644 --- a/tests/lean/run/sec_var.lean +++ b/tests/lean/run/sec_var.lean @@ -1,6 +1,6 @@ import logic -context +section parameter A : Type definition foo : ∀ ⦃ a b : A ⦄, a = b → a = b := take a b H, H diff --git a/tests/lean/run/section3.lean b/tests/lean/run/section3.lean index 3a12c83b5..0623525d2 100644 --- a/tests/lean/run/section3.lean +++ b/tests/lean/run/section3.lean @@ -1,4 +1,4 @@ -context +section parameter (A : Type) definition foo := A theorem bar {X : Type} {A : X} : foo := diff --git a/tests/lean/run/section4.lean b/tests/lean/run/section4.lean index 72b2b1a6c..f70eb4a3b 100644 --- a/tests/lean/run/section4.lean +++ b/tests/lean/run/section4.lean @@ -3,13 +3,13 @@ import logic set_option pp.universes true set_option pp.implicit true -context +section universe k parameter A : Type context - universe l - universe u + universe variable l + universe variable u parameter B : Type definition foo (a : A) (b : B) := b diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean index e2ae78513..623851345 100644 --- a/tests/lean/run/simple.lean +++ b/tests/lean/run/simple.lean @@ -1,6 +1,6 @@ prelude definition Prop : Type.{1} := Type.{0} -context +section parameter A : Type definition eq (a b : A) : Prop diff --git a/tests/lean/run/struct_bug1.lean b/tests/lean/run/struct_bug1.lean index 304ef761c..b2316a988 100644 --- a/tests/lean/run/struct_bug1.lean +++ b/tests/lean/run/struct_bug1.lean @@ -3,7 +3,7 @@ variable (A : Type) structure foo (a : A) := (eqpr : a = a) -context +section parameter (B : Type) structure foo2 (b : B) := diff --git a/tests/lean/run/structure_test.lean b/tests/lean/run/structure_test.lean index fb2acec86..d2ea0389b 100644 --- a/tests/lean/run/structure_test.lean +++ b/tests/lean/run/structure_test.lean @@ -27,7 +27,7 @@ section check point3d_color.to_point end -context +section universe l parameters A : Type.{l} parameters B : Type.{l} diff --git a/tests/lean/run/t11.lean b/tests/lean/run/t11.lean index 80e405181..cd0596e5e 100644 --- a/tests/lean/run/t11.lean +++ b/tests/lean/run/t11.lean @@ -2,7 +2,7 @@ constant A : Type.{1} constants a b c : A constant f : A → A → A check f a b -context +section parameters A B : Type parameters {C D : Type} parameters [e d : A] diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean index 66f4d4592..62c3dfca7 100644 --- a/tests/lean/run/univ1.lean +++ b/tests/lean/run/univ1.lean @@ -19,7 +19,7 @@ end S2 namespace S3 -context +section hypothesis I : Type definition F (X : Type) : Type := (X → Prop) → Prop hypothesis unfold : I → F I diff --git a/tests/lean/run/univs.lean b/tests/lean/run/univs.lean index fb1d21ee2..40abfdb08 100644 --- a/tests/lean/run/univs.lean +++ b/tests/lean/run/univs.lean @@ -1,7 +1,7 @@ import algebra.category.basic set_option pp.universes true -context +section universes l₁ l₂ l₃ l₄ parameter C : Category.{l₁ l₂} parameter f : Category.{l₁ l₂} → Category.{l₃ l₄} diff --git a/tests/lean/sec3.lean b/tests/lean/sec3.lean index ad8f9f749..b5920481a 100644 --- a/tests/lean/sec3.lean +++ b/tests/lean/sec3.lean @@ -1,4 +1,4 @@ -context +section parameter A : Type definition tst (a : A) := a set_option pp.universes true diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean index fc566b95f..448448b2c 100644 --- a/tests/lean/t14.lean +++ b/tests/lean/t14.lean @@ -5,25 +5,25 @@ prelude namespace foo constant c : A end foo -context +section open foo (renaming a->b x->y) (hiding c) check b check y check c -- Error end -context +section open foo (a x) check a check x check c -- Error end -context +section open foo (a x) (hiding c) -- Error end -context +section open foo check a check c @@ -35,18 +35,18 @@ namespace foo infix `*`:75 := f end foo -context +section open foo check a * c end -context +section open [notations] foo -- use only the notation check foo.a * foo.c check a * c -- Error end -context +section open [decls] foo -- use only the declarations check f a c check a*c -- Error diff --git a/tests/lean/t3.lean b/tests/lean/t3.lean index 6f149b856..830f4323f 100644 --- a/tests/lean/t3.lean +++ b/tests/lean/t3.lean @@ -7,13 +7,13 @@ namespace tst end tst print raw Type.{tst.v} print raw Type.{v} -- Error: alias 'v' is not available anymore -context - universe z -- Remark: this is a local universe +section + universe variable z -- Remark: this is a local universe print raw Type.{z} end print raw Type.{z} -- Error: local universe 'z' is gone -context - namespace foo -- Error: we cannot create a namespace inside a context +section + namespace foo -- Error: we cannot create a namespace inside a section end namespace tst print raw Type.{v} -- Remark: alias 'v' is available again diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean index 12ebf8ed6..5f22069d1 100644 --- a/tests/lean/t4.lean +++ b/tests/lean/t4.lean @@ -13,7 +13,7 @@ constant f (a b : N) : N constant len.{l} (A : Type.{l}) (n : N) (v : vec.{l} A n) : N check f check len.{1} -context +section parameter A : Type parameter B : Prop hypothesis H : B diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean index 7e25aae2a..3704d002b 100644 --- a/tests/lean/t7.lean +++ b/tests/lean/t7.lean @@ -1,6 +1,6 @@ prelude definition Prop : Type.{1} := Type.{0} constant and : Prop → Prop → Prop -context +section parameter {A : Type} -- Mark A as implicit parameter parameter R : A → A → Prop parameter B : Type diff --git a/tests/lean/var.lean b/tests/lean/var.lean index 1089a8bdd..e8109d8c4 100644 --- a/tests/lean/var.lean +++ b/tests/lean/var.lean @@ -1,7 +1,7 @@ import logic -context +section variable A : Type parameter a : A end diff --git a/tests/lean/var2.lean b/tests/lean/var2.lean index 836f1151e..6007f7c7a 100644 --- a/tests/lean/var2.lean +++ b/tests/lean/var2.lean @@ -1,7 +1,7 @@ import logic -context +section universe l variable A : Type.{l} variable a : A