From 90bfd84a07d0b427cdaa6cc82a8884499c5eedcd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Sep 2016 14:30:54 -0700 Subject: [PATCH] feat(frontends/lean): Type is now (Type 1) In the standard library, we should use explicit universe variables for universe polymorphic definitions. Users that want to declare universe polymorphic definitions but do not want to provide universe level parameters should use Type _ or Type* --- library/init/alternative.lean | 2 +- library/init/applicative.lean | 8 +- library/init/datatypes.lean | 11 +- library/init/functor.lean | 2 +- library/init/funext.lean | 2 +- library/init/meta/backward.lean | 2 +- library/init/meta/environment.lean | 2 +- library/init/meta/expr.lean | 2 +- library/init/meta/pexpr.lean | 2 +- library/init/meta/simp_tactic.lean | 2 +- library/init/meta/tactic.lean | 2 +- library/init/monad.lean | 4 +- library/init/monad_combinators.lean | 20 +-- library/init/state.lean | 22 +-- library/init/to_string.lean | 22 +-- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/elaborator.cpp | 10 +- src/frontends/lean/old_elaborator.cpp | 8 +- src/frontends/lean/parser.cpp | 2 +- src/frontends/lean/pp.cpp | 25 ++-- src/frontends/lean/util.cpp | 2 +- src/library/placeholder.cpp | 8 +- src/library/placeholder.h | 2 + tests/lean/584a.lean.expected.out | 8 +- tests/lean/584b.lean.expected.out | 8 +- tests/lean/584c.lean.expected.out | 10 +- tests/lean/634.lean | 4 +- tests/lean/634.lean.expected.out | 10 +- tests/lean/634b.lean | 6 +- tests/lean/634b.lean.expected.out | 46 +++--- tests/lean/634c.lean | 6 +- tests/lean/634c.lean.expected.out | 44 +++--- tests/lean/634d.lean.expected.out | 8 +- tests/lean/858.lean.expected.out | 2 +- tests/lean/anc1.lean.expected.out | 12 +- tests/lean/aux_decl_zeta.lean | 4 +- tests/lean/choice_expl.lean.expected.out | 2 +- tests/lean/cls_err.lean.expected.out | 2 +- tests/lean/coe1.lean | 4 +- tests/lean/coe2.lean | 4 +- tests/lean/coe3.lean | 2 +- tests/lean/ctx.lean.expected.out | 2 +- tests/lean/def3.lean.expected.out | 2 +- tests/lean/def4.lean.expected.out | 2 +- tests/lean/elab14.lean.expected.out | 2 +- tests/lean/elab15.lean.expected.out | 4 +- tests/lean/elab3.lean.expected.out | 2 +- tests/lean/elab6.lean.expected.out | 4 +- tests/lean/elab8.lean.expected.out | 12 +- tests/lean/elab9.lean.expected.out | 7 +- tests/lean/eta_bug.lean.expected.out | 2 +- tests/lean/eta_tac.lean.expected.out | 2 +- tests/lean/ftree.lean.expected.out | 4 +- tests/lean/inaccessible.lean | 2 +- tests/lean/inaccessible2.lean | 2 +- tests/lean/instance_cache1.lean.expected.out | 6 +- tests/lean/instance_cache_bug1.lean | 2 +- tests/lean/nary_overload.lean.expected.out | 4 +- tests/lean/no_confusion_type.lean | 2 +- .../lean/no_confusion_type.lean.expected.out | 2 +- tests/lean/notation.lean | 2 +- tests/lean/notation.lean.expected.out | 2 +- tests/lean/notation4.lean | 4 +- tests/lean/notation4.lean.expected.out | 6 +- tests/lean/param_binder_update.lean | 8 +- .../param_binder_update.lean.expected.out | 20 +-- tests/lean/param_binder_update2.lean | 2 +- .../param_binder_update2.lean.expected.out | 8 +- tests/lean/parsing_only.lean.expected.out | 2 +- tests/lean/print_ax1.lean.expected.out | 4 +- tests/lean/print_ax2.lean.expected.out | 4 +- tests/lean/print_ax3.lean.expected.out | 4 +- .../lean/private_structure.lean.expected.out | 8 +- tests/lean/prodtst.lean.expected.out | 2 +- tests/lean/restrict_bug.lean.expected.out | 2 +- tests/lean/run/apply4.lean | 4 +- tests/lean/run/atomic2.lean | 2 +- tests/lean/run/back_chaining3.lean | 2 +- tests/lean/run/basic.lean | 20 +-- tests/lean/run/confuse_ind.lean | 2 +- tests/lean/run/def_brec_reflexive.lean | 2 +- tests/lean/run/e15.lean | 7 +- tests/lean/run/e16.lean | 7 +- tests/lean/run/elab3.lean | 2 +- tests/lean/run/group.lean | 14 +- tests/lean/run/ho.lean | 2 +- tests/lean/run/ind1.lean | 2 +- tests/lean/run/ind2.lean | 2 +- tests/lean/run/ind7.lean | 2 +- tests/lean/run/indbug2.lean | 4 +- tests/lean/run/inst_bug.lean | 8 +- tests/lean/run/interp.lean | 2 +- tests/lean/run/match_expr.lean | 2 +- tests/lean/run/nested_inductive.lean | 36 ++--- tests/lean/run/pack_unpack3.lean | 2 +- tests/lean/run/partial_explicit.lean | 4 +- tests/lean/run/record9.lean | 6 +- tests/lean/run/simple.lean | 2 +- .../run/simplifier_canonize_instances.lean | 8 +- .../simplifier_canonize_subsingletons.lean | 4 +- tests/lean/run/struct_bug1.lean | 6 +- tests/lean/run/structure_test.lean | 4 +- tests/lean/run/t11.lean | 6 +- tests/lean/run/t4.lean | 9 +- tests/lean/run/tc_loop.lean | 4 +- tests/lean/run/univ1.lean | 10 +- tests/lean/run/vm_eval1.lean | 2 +- tests/lean/sec_param_pp.lean | 4 +- tests/lean/struct_class.lean | 4 +- tests/lean/struct_class.lean.expected.out | 140 +++++++++--------- tests/lean/subpp.lean.expected.out | 2 +- tests/lean/t3.lean.expected.out | 20 +-- tests/lean/t6.lean | 2 +- tests/lean/tactic_failure.lean.expected.out | 3 +- tests/lean/tuple.lean | 2 +- tests/lean/tuple.lean.expected.out | 2 +- tests/lean/type_class_bug.lean.expected.out | 10 +- tests/lean/unification_hints1.lean | 10 +- tests/lean/univ.lean | 14 +- tests/lean/univ.lean.expected.out | 16 +- tests/lean/univ_vars.lean.expected.out | 10 +- tests/lean/user_attribute.lean.expected.out | 4 +- tests/lean/var2.lean.expected.out | 2 +- 123 files changed, 468 insertions(+), 455 deletions(-) diff --git a/library/init/alternative.lean b/library/init/alternative.lean index 27a74b4a33..65cc63a4cf 100644 --- a/library/init/alternative.lean +++ b/library/init/alternative.lean @@ -22,5 +22,5 @@ alternative.orelse infixr ` <|> `:2 := orelse attribute [inline] -definition guard {f : Type₁ → Type} [alternative f] (p : Prop) [decidable p] : f unit := +definition guard {f : Type → Type} [alternative f] (p : Prop) [decidable p] : f unit := if p then pure () else failure diff --git a/library/init/applicative.lean b/library/init/applicative.lean index 0882060641..42d4b83843 100644 --- a/library/init/applicative.lean +++ b/library/init/applicative.lean @@ -7,16 +7,16 @@ prelude import init.functor set_option new_elaborator true -structure [class] {u₁ u₂} applicative (F : Type u₁ → Type u₂) extends functor F : Type (max u₁+1 u₂) := -(pure : Π {A : Type u₁}, A → F A) -(seq : Π {A B : Type u₁}, F (A → B) → F A → F B) +structure [class] applicative (F : Type → Type) extends functor F := +(pure : Π {A : Type}, A → F A) +(seq : Π {A B : Type}, F (A → B) → F A → F B) attribute [inline] definition pure {F : Type → Type} [applicative F] {A : Type} : A → F A := applicative.pure F attribute [inline] -definition {u} seq_app {A B : Type u} {F : Type → Type} [applicative F] : F (A → B) → F A → F B := +definition seq_app {A B : Type} {F : Type → Type} [applicative F] : F (A → B) → F A → F B := applicative.seq infixr ` <*> `:2 := seq_app diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 98505f4a16..b478b2455d 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -9,7 +9,6 @@ prelude set_option new_elaborator true notation `Prop` := Type 0 -notation `Type₁` := Type 1 notation `Type₂` := Type 2 notation `Type₃` := Type 3 @@ -18,7 +17,7 @@ universe variables u v inductive poly_unit : Type u | star : poly_unit -inductive unit : Type 1 +inductive unit : Type | star : unit inductive true : Prop @@ -26,7 +25,7 @@ inductive true : Prop inductive false : Prop -inductive empty : Type 1 +inductive empty : Type inductive eq {A : Type u} (a : A) : A → Prop | refl : eq a @@ -78,7 +77,7 @@ mk :: (pr1 : A) (pr2 : B pr1) -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))). -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc). -inductive pos_num : Type 1 +inductive pos_num : Type | one : pos_num | bit1 : pos_num → pos_num | bit0 : pos_num → pos_num @@ -88,7 +87,7 @@ namespace pos_num pos_num.rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) end pos_num -inductive num : Type 1 +inductive num : Type | zero : num | pos : pos_num → num @@ -98,7 +97,7 @@ namespace num num.rec_on a (pos one) (λp, pos (succ p)) end num -inductive bool : Type 1 +inductive bool : Type | ff : bool | tt : bool diff --git a/library/init/functor.lean b/library/init/functor.lean index b54a130f70..5d4db07c6e 100644 --- a/library/init/functor.lean +++ b/library/init/functor.lean @@ -6,7 +6,7 @@ Authors: Luke Nelson and Jared Roesch prelude set_option new_elaborator true -structure [class] functor (F : Type → Type) : Type := +structure [class] functor (F : Type → Type) := (map : Π {A B: Type}, (A → B) → F A → F B) attribute [inline] diff --git a/library/init/funext.lean b/library/init/funext.lean index cd4cc8030e..2c3abbc746 100644 --- a/library/init/funext.lean +++ b/library/init/funext.lean @@ -38,7 +38,7 @@ section private definition fun_setoid (A : Type u) (B : A → Type v) : setoid (Πx : A, B x) := setoid.mk (@function.equiv A B) (function.equiv.is_equivalence A B) - private definition extfun (A : Type u) (B : A → Type v) : Type := + private definition extfun (A : Type u) (B : A → Type v) : Type (imax u v) := quot (fun_setoid A B) private definition fun_to_extfun (f : Π x : A, B x) : extfun A B := diff --git a/library/init/meta/backward.lean b/library/init/meta/backward.lean index 702a662009..882ea3e31d 100644 --- a/library/init/meta/backward.lean +++ b/library/init/meta/backward.lean @@ -7,7 +7,7 @@ prelude import init.meta.tactic init.meta.set_get_option_tactics namespace tactic -meta_constant back_lemmas : Type₁ +meta_constant back_lemmas : Type /- Create a datastructure containing all lemmas tagged as [intro]. Lemmas are indexed using their head-symbol. diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index c56fe7f6bf..285c5920ee 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.meta.declaration init.meta.exceptional -meta_constant environment : Type₁ +meta_constant environment : Type namespace environment /- Create a standard environment using the given trust level -/ diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index e752ad94be..673b7d8132 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -9,7 +9,7 @@ import init.meta.level inductive binder_info | default | implicit | strict_implicit | inst_implicit | other -meta_constant macro_def : Type₁ +meta_constant macro_def : Type /- Reflect a C++ expr object. The VM replaces it with the C++ implementation. -/ inductive expr diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean index a254ab4cf6..2f79d1f68a 100644 --- a/library/init/meta/pexpr.lean +++ b/library/init/meta/pexpr.lean @@ -8,7 +8,7 @@ import init.meta.expr universe variables u /- Quoted expressions. They can be converted into expressions by using a tactic. -/ -meta_constant pexpr : Type₁ +meta_constant pexpr : Type protected meta_constant pexpr.of_expr : expr → pexpr protected meta_constant pexpr.subst : pexpr → pexpr → pexpr diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 09d92ae39b..42c9686cb5 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -9,7 +9,7 @@ import init.meta.tactic namespace tactic open list nat -meta_constant simp_lemmas : Type₁ +meta_constant simp_lemmas : Type /- Create a data-structure containing a simp lemma for every constant in the first list of attributes, and a congr lemma for every constant in the second list of attributes. diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 6d922d1058..247f955559 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.trace init.function init.option init.monad init.alternative init.nat_div import init.meta.exceptional init.meta.format init.meta.environment init.meta.pexpr -meta_constant tactic_state : Type₁ +meta_constant tactic_state : Type namespace tactic_state meta_constant env : tactic_state → environment diff --git a/library/init/monad.lean b/library/init/monad.lean index 4b2de08609..bfcdc78e1e 100644 --- a/library/init/monad.lean +++ b/library/init/monad.lean @@ -7,7 +7,7 @@ prelude import init.applicative init.string init.trace set_option new_elaborator true -structure [class] monad (M : Type → Type) extends functor M : Type := +structure [class] monad (M : Type → Type) extends functor M := (ret : Π {A : Type}, A → M A) (bind : Π {A B : Type}, M A → (A → M B) → M B) @@ -15,7 +15,7 @@ attribute [inline] definition return {M : Type → Type} [monad M] {A : Type} : A → M A := monad.ret M -definition {u} fapp {m : Type → Type} [monad m] {A B : Type u} (f : m (A → B)) (a : m A) : m B := +definition fapp {m : Type → Type} [monad m] {A B : Type} (f : m (A → B)) (a : m A) : m B := do g ← f, b ← a, return (g b) diff --git a/library/init/monad_combinators.lean b/library/init/monad_combinators.lean index 6ed875f69f..a08298d1c6 100644 --- a/library/init/monad_combinators.lean +++ b/library/init/monad_combinators.lean @@ -10,25 +10,25 @@ import init.monad init.list set_option new_elaborator true namespace monad -definition {u} mapM {m : Type → Type} [monad m] {A B : Type (u+1)} (f : A → m B) : list A → m (list B) +definition mapM {m : Type → Type} [monad m] {A B : Type} (f : A → m B) : list A → m (list B) | [] := return [] | (h :: t) := do h' ← f h, t' ← mapM t, return (h' :: t') -definition mapM' {m : Type 1 → Type 1} [monad m] {A B : Type 1} (f : A → m B) : list A → m unit +definition mapM' {m : Type → Type} [monad m] {A B : Type} (f : A → m B) : list A → m unit | [] := return () | (h :: t) := f h >> mapM' t -definition {u} forM {m : Type → Type} [monad m] {A B : Type (u+1)} (l : list A) (f : A → m B) : m (list B) := +definition forM {m : Type → Type} [monad m] {A B : Type} (l : list A) (f : A → m B) : m (list B) := mapM f l -definition forM' {m : Type 1 → Type 1} [monad m] {A B : Type 1} (l : list A) (f : A → m B) : m unit := +definition forM' {m : Type → Type} [monad m] {A B : Type} (l : list A) (f : A → m B) : m unit := mapM' f l -definition {u} sequence {m : Type → Type} [monad m] {A : Type (u+1)} : list (m A) → m (list A) +definition sequence {m : Type → Type} [monad m] {A : Type} : list (m A) → m (list A) | [] := return [] | (h :: t) := do h' ← h, t' ← sequence t, return (h' :: t') -definition sequence' {m : Type 1 → Type 1} [monad m] {A : Type 1} : list (m A) → m unit +definition sequence' {m : Type → Type} [monad m] {A : Type} : list (m A) → m unit | [] := return () | (h :: t) := h >> sequence' t @@ -41,17 +41,17 @@ infix ` <=< `:2 := λ t s a, s a >>= t definition join {m : Type → Type} [monad m] {A : Type} (a : m (m A)) : m A := bind a id -definition filterM {m : Type₁ → Type₁} [monad m] {A : Type₁} (f : A → m bool) : list A → m (list A) +definition filterM {m : Type → Type} [monad m] {A : Type} (f : A → m bool) : list A → m (list A) | [] := return [] | (h :: t) := do b ← f h, t' ← filterM t, bool.cond b (return (h :: t')) (return t') -definition whenb {m : Type₁ → Type₁} [monad m] (b : bool) (t : m unit) : m unit := +definition whenb {m : Type → Type} [monad m] (b : bool) (t : m unit) : m unit := bool.cond b t (return ()) -definition unlessb {m : Type₁ → Type₁} [monad m] (b : bool) (t : m unit) : m unit := +definition unlessb {m : Type → Type} [monad m] (b : bool) (t : m unit) : m unit := bool.cond b (return ()) t -definition condM {m : Type₁ → Type₁} [monad m] {A : Type₁} (mbool : m bool) +definition condM {m : Type → Type} [monad m] {A : Type} (mbool : m bool) (tm fm : m A) : m A := do b ← mbool, bool.cond b tm fm diff --git a/library/init/state.lean b/library/init/state.lean index 9af3a8c450..a482ee2df6 100644 --- a/library/init/state.lean +++ b/library/init/state.lean @@ -9,6 +9,7 @@ set_option new_elaborator true definition state (S : Type) (A : Type) := S → A × S section +set_option pp.all true variables {S A B : Type} attribute [inline] @@ -41,36 +42,35 @@ end state definition stateT (S : Type) (m : Type → Type) [monad m] (A : Type) := S → m (A × S) section - universe variables u₁ u₂ - variable {S : Type u₂} - variable {m : Type (max 1 u₁ u₂) → Type} + variable {S : Type} + variable {m : Type → Type} variable [monad m] - variables {A B : Type u₁} + variables {A B : Type} - definition stateT_fmap (f : A → B) (act : stateT.{u₂ u₁} S m A) : stateT.{u₂ u₁} S m B := + definition stateT_fmap (f : A → B) (act : stateT S m A) : stateT S m B := λ s, show m (B × S), from do (a, new_s) ← act s, return (f a, new_s) - definition stateT_return (a : A) : stateT.{u₂ u₁} S m A := + definition stateT_return (a : A) : stateT S m A := λ s, show m (A × S), from return (a, s) - definition stateT_bind (act₁ : stateT.{u₂ u₁} S m A) (act₂ : A → stateT.{u₂ u₁} S m B) : stateT.{u₂ u₁} S m B := + definition stateT_bind (act₁ : stateT S m A) (act₂ : A → stateT S m B) : stateT S m B := λ s, show m (B × S), from do (a, new_s) ← act₁ s, act₂ a new_s end attribute [instance] -definition {u} stateT_is_monad (S : Type u) (m : Type → Type) [monad m] : monad (stateT S m) := -monad.mk (@stateT_fmap.{_ u} S m _) (@stateT_return.{_ u} S m _) (@stateT_bind.{_ u} S m _) +definition stateT_is_monad (S : Type) (m : Type → Type) [monad m] : monad (stateT S m) := +monad.mk (@stateT_fmap S m _) (@stateT_return S m _) (@stateT_bind S m _) set_option pp.all true namespace stateT -definition {u} read {S : Type u} {m : Type (max 1 u) → Type} [monad m] : stateT.{u u} S m S := +definition read {S : Type} {m : Type → Type} [monad m] : stateT S m S := λ s, return (s, s) -definition {u} write {S : Type u} {m : Type (max 1 u) → Type} [monad m] : S → stateT.{u 1} S m unit := +definition write {S : Type} {m : Type → Type} [monad m] : S → stateT S m unit := λ s' s, return ((), s') end stateT diff --git a/library/init/to_string.lean b/library/init/to_string.lean index 4ca2385cf0..cdadad3121 100644 --- a/library/init/to_string.lean +++ b/library/init/to_string.lean @@ -6,10 +6,12 @@ import init.string init.bool init.subtype init.unsigned init.prod init.sum set_option new_elaborator true open bool list sum prod sigma subtype nat -structure [class] has_to_string (A : Type) := +universe variables u v + +structure [class] has_to_string (A : Type u) := (to_string : A → string) -definition to_string {A : Type} [has_to_string A] : A → string := +definition to_string {A : Type u} [has_to_string A] : A → string := has_to_string.to_string attribute [instance] @@ -21,17 +23,17 @@ definition decidable.has_to_string {p : Prop} : has_to_string (decidable p) := -- Remark: type class inference will not consider local instance `b` in the new elaborator has_to_string.mk (λ b : decidable p, @ite p b _ "tt" "ff") -definition list.to_string_aux {A : Type} [has_to_string A] : bool → list A → string +definition list.to_string_aux {A : Type u} [has_to_string A] : bool → list A → string | b [] := "" | tt (x::xs) := to_string x ++ list.to_string_aux ff xs | ff (x::xs) := ", " ++ to_string x ++ list.to_string_aux ff xs -definition list.to_string {A : Type} [has_to_string A] : list A → string +definition list.to_string {A : Type u} [has_to_string A] : list A → string | [] := "[]" | (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]" attribute [instance] -definition list.has_to_string {A : Type} [has_to_string A] : has_to_string (list A) := +definition list.has_to_string {A : Type u} [has_to_string A] : has_to_string (list A) := has_to_string.mk list.to_string attribute [instance] @@ -39,24 +41,24 @@ definition unit.has_to_string : has_to_string unit := has_to_string.mk (λ u, "star") attribute [instance] -definition option.has_to_string {A : Type} [has_to_string A] : has_to_string (option A) := +definition option.has_to_string {A : Type u} [has_to_string A] : has_to_string (option A) := has_to_string.mk (λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")" end) attribute [instance] -definition sum.has_to_string {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (A ⊕ B) := +definition sum.has_to_string {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A ⊕ B) := has_to_string.mk (λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")" end) attribute [instance] -definition prod.has_to_string {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (A × B) := +definition prod.has_to_string {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A × B) := has_to_string.mk (λ p, "(" ++ to_string (pr1 p) ++ ", " ++ to_string (pr2 p) ++ ")") attribute [instance] -definition sigma.has_to_string {A : Type} {B : A → Type} [has_to_string A] [s : ∀ x, has_to_string (B x)] +definition sigma.has_to_string {A : Type u} {B : A → Type v} [has_to_string A] [s : ∀ x, has_to_string (B x)] : has_to_string (sigma B) := has_to_string.mk (λ p, "⟨" ++ to_string (pr1 p) ++ ", " ++ to_string (pr2 p) ++ "⟩") attribute [instance] -definition subtype.has_to_string {A : Type} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) := +definition subtype.has_to_string {A : Type u} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) := has_to_string.mk (λ s, to_string (elt_of s)) definition char.quote_core (c : char) : string := diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 9f535bf10e..3f005842c3 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -53,7 +53,7 @@ static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) p.check_token_next(get_rcurly_tk(), "invalid Type expression, '}' expected"); return p.save_pos(mk_sort(l), pos); } else { - return p.save_pos(mk_sort(mk_level_placeholder()), pos); + return p.save_pos(mk_sort(mk_level_one_placeholder()), pos); } } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1cbe3661cb..7abb8b705d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -210,7 +210,9 @@ level elaborator::get_level(expr const & A, expr const & ref) { level elaborator::replace_univ_placeholder(level const & l) { auto fn = [&](level const & l) { - if (is_placeholder(l)) + if (is_one_placeholder(l)) + return some_level(mk_level_one()); + else if (is_placeholder(l)) return some_level(mk_univ_metavar()); else return none_level(); @@ -222,7 +224,7 @@ static bool contains_placeholder(level const & l) { bool contains = false; auto fn = [&](level const & l) { if (contains) return false; - if (is_placeholder(l)) + if (is_placeholder(l) || is_one_placeholder(l)) contains = true; return true; }; @@ -2084,7 +2086,7 @@ void elaborator::snapshot::restore(elaborator & e) { into parameters */ struct sanitize_param_names_fn : public replace_visitor { type_context & m_ctx; - name m_p{"l"}; + name m_p{"u"}; name_set m_L; /* All parameter names in the input expression. */ name_map m_R; /* map from tagged g_level_prefix to "clean" name not in L. */ name_map m_U; /* map from universe metavariable name to "clean" name not in L. */ @@ -2107,7 +2109,7 @@ struct sanitize_param_names_fn : public replace_visitor { } level sanitize(level const & l) { - name p("l"); + name p("u"); return replace(l, [&](level const & l) -> optional { if (is_param(l)) { name const & n = param_id(l); diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index 0e3f57e824..380668b5e5 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -585,7 +585,9 @@ expr old_elaborator::visit_placeholder(expr const & e, constraint_seq & cs) { level old_elaborator::replace_univ_placeholder(level const & l) { auto fn = [&](level const & l) { - if (is_placeholder(l)) + if (is_one_placeholder(l)) + return some_level(mk_level_one()); + else if (is_placeholder(l)) return some_level(mk_meta_univ(mk_fresh_name())); else return none_level(); @@ -597,7 +599,7 @@ static bool contains_placeholder(level const & l) { bool contains = false; auto fn = [&](level const & l) { if (contains) return false; - if (is_placeholder(l)) + if (is_placeholder(l) || is_one_placeholder(l)) contains = true; return true; }; @@ -1511,7 +1513,7 @@ optional old_elaborator::execute_tactic(expr const & tactic, tacti scope_elaborate_fn scope(fn); name tactic_name("_tactic"); - expr tactic_type = ::lean::mk_app(mk_constant("tactic", {mk_level_one()}), mk_constant("unit")); + expr tactic_type = ::lean::mk_app(mk_constant("tactic"), mk_constant("unit")); /* compile tactic */ environment new_env = env(); options const & opts = m_ctx.m_options; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0d0dda9b75..f8b05fb6d9 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2107,7 +2107,7 @@ bool parser::curr_starts_expr() { } expr parser::parse_led(expr left) { - if (is_sort(left) && is_placeholder(sort_level(left)) && + if (is_sort(left) && is_one_placeholder(sort_level(left)) && (curr_is_numeral() || curr_is_identifier() || curr_is_token(get_lparen_tk()) || curr_is_token(get_placeholder_tk()))) { level l = parse_level(get_max_prec()); return copy_tag(left, update_sort(left, l)); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 31987620f4..4664b0ffab 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -359,12 +359,16 @@ format pretty_fn::pp_max(level l) { } format pretty_fn::pp_meta(level const & l) { - if (is_idx_metauniv(l)) { - return format((sstream() << "?u_" << to_meta_idx(l)).str()); - } else if (is_metavar_decl_ref(l)) { - return format((sstream() << "?l_" << get_metavar_decl_ref_suffix(l)).str()); + if (m_universes) { + if (is_idx_metauniv(l)) { + return format((sstream() << "?u_" << to_meta_idx(l)).str()); + } else if (is_metavar_decl_ref(l)) { + return format((sstream() << "?l_" << get_metavar_decl_ref_suffix(l)).str()); + } else { + return compose(format("?"), format(meta_id(l))); + } } else { - return compose(format("?"), format(meta_id(l))); + return format("?"); } } @@ -604,12 +608,13 @@ auto pretty_fn::pp_var(expr const & e) -> result { } auto pretty_fn::pp_sort(expr const & e) -> result { - if (m_env.impredicative() && e == mk_Prop()) { - return result(format("Prop")); - } else if (m_universes) { - return result(group(format("Type.{") + nest(6, pp_level(sort_level(e))) + format("}"))); - } else { + level u = sort_level(e); + if (u == mk_level_zero()) { + return m_env.impredicative() ? result(format("Prop")) : result(format("Type")); + } else if (m_env.impredicative() && u == mk_level_one()) { return result(format("Type")); + } else { + return result(group(format("Type") + space() + nest(5, pp_child(u)))); } } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index b7e7700bf2..4a4189b721 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -416,6 +416,6 @@ pair parse_option_name(parser & p, char const * error_msg) { } expr mk_tactic_unit() { - return mk_app(mk_constant(get_tactic_name(), {mk_level_one()}), mk_constant(get_unit_name())); + return mk_app(mk_constant(get_tactic_name()), mk_constant(get_unit_name())); } } diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index f9ef1fe4a4..5be3acf409 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -9,12 +9,14 @@ Author: Leonardo de Moura #include "library/placeholder.h" namespace lean { +static name * g_placeholder_one_name = nullptr; static name * g_implicit_placeholder_name = nullptr; static name * g_placeholder_name = nullptr; static name * g_strict_placeholder_name = nullptr; static name * g_explicit_placeholder_name = nullptr; void initialize_placeholder() { + g_placeholder_one_name = new name(name::mk_internal_unique_name(), "_"); g_implicit_placeholder_name = new name(name::mk_internal_unique_name(), "_"); g_placeholder_name = g_implicit_placeholder_name; g_strict_placeholder_name = new name(name::mk_internal_unique_name(), "_"); @@ -25,6 +27,7 @@ void finalize_placeholder() { delete g_implicit_placeholder_name; delete g_strict_placeholder_name; delete g_explicit_placeholder_name; + delete g_placeholder_one_name; } LEAN_THREAD_VALUE(unsigned, g_placeholder_id, 0); @@ -34,6 +37,7 @@ static unsigned next_placeholder_id() { return r; } level mk_level_placeholder() { return mk_global_univ(name(*g_placeholder_name, next_placeholder_id())); } +level mk_level_one_placeholder() { return mk_global_univ(*g_placeholder_one_name); } static name const & to_prefix(expr_placeholder_kind k) { switch (k) { case expr_placeholder_kind::Implicit: return *g_implicit_placeholder_name; @@ -62,6 +66,8 @@ static bool is_explicit_placeholder(name const & n) { return !n.is_atomic() && n.get_prefix() == *g_explicit_placeholder_name; } bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); } +bool is_one_placeholder(level const & e) { return is_global(e) && global_id(e) == *g_placeholder_one_name; } + bool is_placeholder(expr const & e) { return (is_constant(e) && is_placeholder(const_name(e))) || (is_local(e) && is_placeholder(mlocal_name(e))); } @@ -81,7 +87,7 @@ optional placeholder_type(expr const & e) { bool has_placeholder(level const & l) { bool r = false; for_each(l, [&](level const & e) { - if (is_placeholder(e)) + if (is_placeholder(e) || is_one_placeholder(e)) r = true; return !r; }); diff --git a/src/library/placeholder.h b/src/library/placeholder.h index d8e239086c..db8777ab6f 100644 --- a/src/library/placeholder.h +++ b/src/library/placeholder.h @@ -12,6 +12,7 @@ Author: Leonardo de Moura namespace lean { /** \brief Return a new universe level placeholder. */ level mk_level_placeholder(); +level mk_level_one_placeholder(); enum class expr_placeholder_kind { Implicit, StrictImplicit, Explicit }; /** \brief Return a new expression placeholder expression. */ @@ -25,6 +26,7 @@ inline expr mk_strict_expr_placeholder(optional const & type = none_expr() /** \brief Return true if the given level is a placeholder. */ bool is_placeholder(level const & e); +bool is_one_placeholder(level const & e); /** \brief Return true iff the given expression is a placeholder (strict, explicit or implicit). */ bool is_placeholder(expr const & e); diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out index 699a69119f..c8171e3c71 100644 --- a/tests/lean/584a.lean.expected.out +++ b/tests/lean/584a.lean.expected.out @@ -1,5 +1,5 @@ -foo : Π (A : Type) [H : inhabited A], A → A -foo' : Π {A : Type} [H : inhabited A] {x : A}, A +foo : Π (A : Type u_1) [H : inhabited A], A → A +foo' : Π {A : Type u_1} [H : inhabited A] {x : A}, A foo ℕ 10 : ℕ -definition test : ∀ {A : Type} [H : inhabited A], @foo' ℕ nat.is_inhabited (5 + 5) = 10 := -λ {A : Type} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.is_inhabited (5 + 5)) +definition test : ∀ {A : Type u} [H : inhabited A], @foo' ℕ nat.is_inhabited (5 + 5) = 10 := +λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.is_inhabited (5 + 5)) diff --git a/tests/lean/584b.lean.expected.out b/tests/lean/584b.lean.expected.out index 6fd6153f00..1780d281c3 100644 --- a/tests/lean/584b.lean.expected.out +++ b/tests/lean/584b.lean.expected.out @@ -1,4 +1,4 @@ -tst₁ : Π (A : Type), A → A -tst₂ : Π {A : Type}, A → A -symm₂ : ∀ {A : Type} (a b : A), a = b → b = a -tst₃ : Π (A : Type), A → A +tst₁ : Π (A : Type u_1), A → A +tst₂ : Π {A : Type u_1}, A → A +symm₂ : ∀ {A : Type u_1} (a b : A), a = b → b = a +tst₃ : Π (A : Type u_1), A → A diff --git a/tests/lean/584c.lean.expected.out b/tests/lean/584c.lean.expected.out index e12d00ae68..a7f415d768 100644 --- a/tests/lean/584c.lean.expected.out +++ b/tests/lean/584c.lean.expected.out @@ -1,5 +1,5 @@ -tst₁ : Π (A : Type), A → A -tst₂ : Π {A : Type}, A → A -symm₂ : ∀ {A : Type} (a b : A), a = b → b = a -tst₃ : Π (A : Type), A → A -foo : ∀ {A : Type} {a b : A}, a = b → ∀ (c : A), c = b → c = a +tst₁ : Π (A : Type u_1), A → A +tst₂ : Π {A : Type u_1}, A → A +symm₂ : ∀ {A : Type u_1} (a b : A), a = b → b = a +tst₃ : Π (A : Type u_1), A → A +foo : ∀ {A : Type u_1} {a b : A}, a = b → ∀ (c : A), c = b → c = a diff --git a/tests/lean/634.lean b/tests/lean/634.lean index 8c213d0e2a..5ff60981bb 100644 --- a/tests/lean/634.lean +++ b/tests/lean/634.lean @@ -1,8 +1,8 @@ open nat namespace foo section - parameter (X : Type₁) - definition A {n : ℕ} : Type₁ := X + parameter (X : Type) + definition A {n : ℕ} : Type := X variable {n : ℕ} set_option pp.implicit true check @A n diff --git a/tests/lean/634.lean.expected.out b/tests/lean/634.lean.expected.out index 22408b39e3..111dcb3987 100644 --- a/tests/lean/634.lean.expected.out +++ b/tests/lean/634.lean.expected.out @@ -1,5 +1,5 @@ -@A n : Type₁ -@foo.A X n : Type₁ -@foo.A X n : Type₁ -@A n : Type₁ -@A n : Type₁ +@A n : Type +@foo.A X n : Type +@foo.A X n : Type +@A n : Type +@A n : Type diff --git a/tests/lean/634b.lean b/tests/lean/634b.lean index 097699ca28..d841392ba9 100644 --- a/tests/lean/634b.lean +++ b/tests/lean/634b.lean @@ -1,9 +1,9 @@ open nat namespace foo section - parameter (X : Type₁) - definition A {n : ℕ} : Type₁ := X - definition B : Type₁ := X + parameter (X : Type) + definition A {n : ℕ} : Type := X + definition B : Type := X variable {n : ℕ} check @A n check foo.A nat diff --git a/tests/lean/634b.lean.expected.out b/tests/lean/634b.lean.expected.out index 26bc0b02dc..1d798e7c43 100644 --- a/tests/lean/634b.lean.expected.out +++ b/tests/lean/634b.lean.expected.out @@ -1,23 +1,23 @@ -A : Type₁ -foo.A ℕ : Type₁ -foo.A (X × B) : Type₁ -foo.A (X × B) : Type₁ -foo.A (foo.B A) : Type₁ -foo.A (foo.B A) : Type₁ -foo.A (foo.B (foo.A ℕ)) : Type₁ -foo.A X : Type₁ -foo.A ℕ : Type₁ -foo.A (X × foo.B X) : Type₁ -foo.A (foo.B (foo.A X)) : Type₁ -foo.A (foo.B (foo.A ℕ)) : Type₁ -@A n : Type₁ -@foo.A ℕ 10 : Type₁ -@A n : Type₁ -@foo.A X n : Type₁ -@foo.A X n : Type₁ -@A n : Type₁ -@foo.A B n : Type₁ -@foo.A (foo.B (@A n)) n : Type₁ -@foo.A (foo.B (@A n)) n : Type₁ -@foo.A (foo.B (@foo.A ℕ n)) n : Type₁ -@A n : Type₁ +A : Type +foo.A ℕ : Type +foo.A (X × B) : Type +foo.A (X × B) : Type +foo.A (foo.B A) : Type +foo.A (foo.B A) : Type +foo.A (foo.B (foo.A ℕ)) : Type +foo.A X : Type +foo.A ℕ : Type +foo.A (X × foo.B X) : Type +foo.A (foo.B (foo.A X)) : Type +foo.A (foo.B (foo.A ℕ)) : Type +@A n : Type +@foo.A ℕ 10 : Type +@A n : Type +@foo.A X n : Type +@foo.A X n : Type +@A n : Type +@foo.A B n : Type +@foo.A (foo.B (@A n)) n : Type +@foo.A (foo.B (@A n)) n : Type +@foo.A (foo.B (@foo.A ℕ n)) n : Type +@A n : Type diff --git a/tests/lean/634c.lean b/tests/lean/634c.lean index 40c6a6bc6d..32ae348a77 100644 --- a/tests/lean/634c.lean +++ b/tests/lean/634c.lean @@ -1,8 +1,8 @@ open nat section - parameter (X : Type₁) - definition A {n : ℕ} : Type₁ := X - definition B : Type₁ := X + parameter (X : Type) + definition A {n : ℕ} : Type := X + definition B : Type := X variable {n : ℕ} check @A n check _root_.A nat diff --git a/tests/lean/634c.lean.expected.out b/tests/lean/634c.lean.expected.out index 1bf0eee20d..69045bddc5 100644 --- a/tests/lean/634c.lean.expected.out +++ b/tests/lean/634c.lean.expected.out @@ -1,22 +1,22 @@ -A : Type₁ -_root_.A ℕ : Type₁ -_root_.A (X × B) : Type₁ -_root_.A (X × B) : Type₁ -_root_.A (_root_.B A) : Type₁ -_root_.A (_root_.B (_root_.A ℕ)) : Type₁ -A : Type₁ -_root_.A ℕ : Type₁ -_root_.A (X × B) : Type₁ -_root_.A (_root_.B A) : Type₁ -_root_.A (_root_.B (_root_.A ℕ)) : Type₁ -@A n : Type₁ -@_root_.A ℕ 10 : Type₁ -@A n : Type₁ -@A n : Type₁ -@_root_.A B n : Type₁ -@A n : Type₁ -@_root_.A B n : Type₁ -@_root_.A (_root_.B (@A n)) n : Type₁ -@_root_.A (_root_.B (@A n)) n : Type₁ -@_root_.A (_root_.B (@_root_.A ℕ n)) n : Type₁ -@A n : Type₁ +A : Type +_root_.A ℕ : Type +_root_.A (X × B) : Type +_root_.A (X × B) : Type +_root_.A (_root_.B A) : Type +_root_.A (_root_.B (_root_.A ℕ)) : Type +A : Type +_root_.A ℕ : Type +_root_.A (X × B) : Type +_root_.A (_root_.B A) : Type +_root_.A (_root_.B (_root_.A ℕ)) : Type +@A n : Type +@_root_.A ℕ 10 : Type +@A n : Type +@A n : Type +@_root_.A B n : Type +@A n : Type +@_root_.A B n : Type +@_root_.A (_root_.B (@A n)) n : Type +@_root_.A (_root_.B (@A n)) n : Type +@_root_.A (_root_.B (@_root_.A ℕ n)) n : Type +@A n : Type diff --git a/tests/lean/634d.lean.expected.out b/tests/lean/634d.lean.expected.out index 52d9ff84cc..3486b1fdeb 100644 --- a/tests/lean/634d.lean.expected.out +++ b/tests/lean/634d.lean.expected.out @@ -1,7 +1,7 @@ -A : Type → Type -_root_.A : Type₁ → Type₁ -A : Type.{l} → Type.{l} -_root_.A.{1} : Type₁ → Type₁ +A : Type l → Type l +_root_.A : Type → Type +A : Type l → Type l +_root_.A.{1} : Type → Type P : B → B _root_.P : Π {n : ℕ}, ℕ → ℕ P : B → B diff --git a/tests/lean/858.lean.expected.out b/tests/lean/858.lean.expected.out index 784c6ef931..98a8fffe95 100644 --- a/tests/lean/858.lean.expected.out +++ b/tests/lean/858.lean.expected.out @@ -1,3 +1,3 @@ 858.lean:2:18: error: don't know how to synthesize placeholder state: -⊢ Type +⊢ Type ? diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index e8d3b48226..0fe8cd86dc 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/tests/lean/anc1.lean.expected.out @@ -14,12 +14,12 @@ Exists.intro 1 (λ (a : 1 = 0), nat.no_confusion a) : ∃ (x : ℕ), 1 ≠ 0 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show ((B ∧ true) ∧ A) ∧ C ∧ A, from and.intro (and.intro (and.intro Hb true.intro) Ha) (and.intro Hc Ha) : ∀ (A B C : Prop), A → B → C → ((B ∧ true) ∧ A) ∧ C ∧ A -λ (A : Type) (P Q : A → Prop) (a : A) (H1 : P a) (H2 : Q a), +λ (A : Type u) (P Q : A → Prop) (a : A) (H1 : P a) (H2 : Q a), show ∃ (x : A), P x ∧ Q x, from Exists.intro a (and.intro H1 H2) : - ∀ (A : Type) (P Q : A → Prop) (a : A), P a → Q a → (∃ (x : A), P x ∧ Q x) -λ (A : Type) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b), + ∀ (A : Type u) (P Q : A → Prop) (a : A), P a → Q a → (∃ (x : A), P x ∧ Q x) +λ (A : Type u) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b), show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) : - ∀ (A : Type) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y) -λ (A : Type) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b), + ∀ (A : Type u) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y) +λ (A : Type u) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b), show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) : - ∀ (A : Type) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y) + ∀ (A : Type u) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y) diff --git a/tests/lean/aux_decl_zeta.lean b/tests/lean/aux_decl_zeta.lean index 0a6dc843fe..817e14b3d1 100644 --- a/tests/lean/aux_decl_zeta.lean +++ b/tests/lean/aux_decl_zeta.lean @@ -1,6 +1,6 @@ set_option new_elaborator true -universe variables u -inductive vec (A : Type u) : nat → Type + +inductive vec (A : Type*) : nat → Type* | nil : vec 0 | cons : Π {n}, A → vec n → vec (n+1) diff --git a/tests/lean/choice_expl.lean.expected.out b/tests/lean/choice_expl.lean.expected.out index 209226e246..f861e790f5 100644 --- a/tests/lean/choice_expl.lean.expected.out +++ b/tests/lean/choice_expl.lean.expected.out @@ -1,4 +1,4 @@ -pr : Π {A : Type}, A → A → A +pr : Π {A : Type u_1}, A → A → A pr a b : N choice_expl.lean:16:6: error: ambiguous overload, possible interpretations N2.pr a b diff --git a/tests/lean/cls_err.lean.expected.out b/tests/lean/cls_err.lean.expected.out index 73aa9b312a..e61e7d5f80 100644 --- a/tests/lean/cls_err.lean.expected.out +++ b/tests/lean/cls_err.lean.expected.out @@ -1,3 +1,3 @@ cls_err.lean:13:2: error: failed to synthesize placeholder -A : Type +A : Type u ⊢ H A diff --git a/tests/lean/coe1.lean b/tests/lean/coe1.lean index 580e6818bc..3f402f4acc 100644 --- a/tests/lean/coe1.lean +++ b/tests/lean/coe1.lean @@ -2,8 +2,8 @@ check if tt then "a" else "b" /- Remark: in the standard library nat_to_int and int_to_real are has_lift instances instead of has_coe. -/ -constant int : Type₁ -constant real : Type₁ +constant int : Type +constant real : Type constant nat_to_int : has_coe nat int constant int_to_real : has_coe int real attribute [instance] nat_to_int int_to_real diff --git a/tests/lean/coe2.lean b/tests/lean/coe2.lean index 41639d60af..0ed74e74bf 100644 --- a/tests/lean/coe2.lean +++ b/tests/lean/coe2.lean @@ -4,8 +4,8 @@ check if tt then "a" else "b" /- Remark: in the standard library nat_to_int and int_to_real are has_lift instances instead of has_coe. -/ -constant int : Type₁ -constant real : Type₁ +constant int : Type +constant real : Type constant nat_to_int : has_coe nat int constant int_to_real : has_coe int real attribute [instance] nat_to_int int_to_real diff --git a/tests/lean/coe3.lean b/tests/lean/coe3.lean index 553333f7ef..700f0d2513 100644 --- a/tests/lean/coe3.lean +++ b/tests/lean/coe3.lean @@ -1,4 +1,4 @@ -constants A B₁ B₂ C D : Type₁ +constants A B₁ B₂ C D : Type constant A_to_B₁ : has_coe A B₁ constant A_to_B₂ : has_coe A B₂ diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out index cc78fc83cc..c2e57f6d70 100644 --- a/tests/lean/ctx.lean.expected.out +++ b/tests/lean/ctx.lean.expected.out @@ -1,6 +1,6 @@ ctx.lean:3:0: error: don't know how to synthesize placeholder state: -A B : Type, +A B : Type u, a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : ℕ, b1 b2 b3 : bool, h : A = B, diff --git a/tests/lean/def3.lean.expected.out b/tests/lean/def3.lean.expected.out index 345a262b86..d854b17aca 100644 --- a/tests/lean/def3.lean.expected.out +++ b/tests/lean/def3.lean.expected.out @@ -1 +1 @@ -f : Π (A : Type), A → A +f : Π (A : Type u_1), A → A diff --git a/tests/lean/def4.lean.expected.out b/tests/lean/def4.lean.expected.out index 87d4cbd46c..b6632b2840 100644 --- a/tests/lean/def4.lean.expected.out +++ b/tests/lean/def4.lean.expected.out @@ -16,6 +16,6 @@ has type ℕ but is expected to have type A -f : Π (A : Type), A → A +f : Π (A : Type u_1), A → A f ℕ 0 : ℕ g 0 : ℕ diff --git a/tests/lean/elab14.lean.expected.out b/tests/lean/elab14.lean.expected.out index 72b1dd9d71..200985f454 100644 --- a/tests/lean/elab14.lean.expected.out +++ b/tests/lean/elab14.lean.expected.out @@ -1 +1 @@ -λ (A B : Type.{u}) (a : A) (b : B), a : Π (A B : Type.{u}), A → B → A +λ (A B : Type u) (a : A) (b : B), a : Π (A B : Type u), A → B → A diff --git a/tests/lean/elab15.lean.expected.out b/tests/lean/elab15.lean.expected.out index 5a731574de..0996fbcfbd 100644 --- a/tests/lean/elab15.lean.expected.out +++ b/tests/lean/elab15.lean.expected.out @@ -1,4 +1,4 @@ -λ (A : Type) (a b c d : A) (H₁ : eq a b) (H₂ : eq c b) (H₃ : eq d c), +λ (A : Type u) (a b c d : A) (H₁ : eq a b) (H₂ : eq c b) (H₃ : eq d c), have this : eq a c, from eq.trans H₁ (eq.symm H₂), show eq a d, from eq.trans this (eq.symm H₃) : - ∀ (A : Type) (a b c d : A), eq a b → eq c b → eq d c → eq a d + ∀ (A : Type u) (a b c d : A), eq a b → eq c b → eq d c → eq a d diff --git a/tests/lean/elab3.lean.expected.out b/tests/lean/elab3.lean.expected.out index fe75dbc9e6..71b317f44c 100644 --- a/tests/lean/elab3.lean.expected.out +++ b/tests/lean/elab3.lean.expected.out @@ -1 +1 @@ -@monad.and_then.{1 1} unit unit tactic.{1} tactic_is_monad.{1} tactic.trace_state tactic.trace_state : tactic.{1} unit +@monad.and_then unit unit tactic tactic_is_monad tactic.trace_state tactic.trace_state : tactic unit diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/elab6.lean.expected.out index ce016caf6f..a0f59dfc23 100644 --- a/tests/lean/elab6.lean.expected.out +++ b/tests/lean/elab6.lean.expected.out @@ -1,10 +1,10 @@ H : @transitive.{1} nat R -@F.{l_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1 +@F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1 @F.{1} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool @F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool @F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool H : @transitive.{1} nat R -@F.{l_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1 +@F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1 @F.{1} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool @F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool @F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool diff --git a/tests/lean/elab8.lean.expected.out b/tests/lean/elab8.lean.expected.out index 47e1e86cbe..e0b3159a1c 100644 --- a/tests/lean/elab8.lean.expected.out +++ b/tests/lean/elab8.lean.expected.out @@ -1,14 +1,14 @@ -λ (A : Type) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A] (a : A), +λ (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A] (a : A), @add A _inst_1 a (@one A _inst_2) : - Π (A : Type) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A], A → A -λ (A : Type) [_inst_4 : has_add A] [_inst_5 : has_one A] [_inst_6 : has_lt A] (a : A) + Π (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A], A → A +λ (A : Type u_1) [_inst_4 : has_add A] [_inst_5 : has_one A] [_inst_6 : has_lt A] (a : A) (H : @gt A _inst_6 a (@one A _inst_5)), @add A _inst_4 a (@one A _inst_5) : - Π (A : Type) [_inst_4 : has_add A] [_inst_5 : has_one A] [_inst_6 : has_lt A] (a : A), + Π (A : Type u_1) [_inst_4 : has_add A] [_inst_5 : has_one A] [_inst_6 : has_lt A] (a : A), @gt A _inst_6 a (@one A _inst_5) → A -λ (A : Type) [_inst_7 : has_add A] [_inst_8 : has_one A] [_inst_9 : has_lt A] (a : A) +λ (A : Type u_1) [_inst_7 : has_add A] [_inst_8 : has_one A] [_inst_9 : has_lt A] (a : A) (H₁ : @gt A _inst_9 a (@one A _inst_8)) (H₂ : @lt A _inst_9 a (@bit1 A _inst_8 _inst_7 (@bit0 A _inst_7 (@one A _inst_8)))), @add A _inst_7 a (@one A _inst_8) : - Π (A : Type) [_inst_7 : has_add A] [_inst_8 : has_one A] [_inst_9 : has_lt A] (a : A), + Π (A : Type u_1) [_inst_7 : has_add A] [_inst_8 : has_one A] [_inst_9 : has_lt A] (a : A), @gt A _inst_9 a (@one A _inst_8) → @lt A _inst_9 a (@bit1 A _inst_8 _inst_7 (@bit0 A _inst_7 (@one A _inst_8))) → A diff --git a/tests/lean/elab9.lean.expected.out b/tests/lean/elab9.lean.expected.out index 8a3840f78b..0279f0b76d 100644 --- a/tests/lean/elab9.lean.expected.out +++ b/tests/lean/elab9.lean.expected.out @@ -1,6 +1,7 @@ -λ (A : Type) [_inst_1 : has_add A] [_inst_2 : has_zero A] (a : A) (H : @eq A (@add A _inst_1 a (@zero A _inst_2)) a) -[_inst_3 : has_add A] (H : @eq A a (@add A _inst_3 (@zero A _inst_2) (@zero A _inst_2))), @add A _inst_3 a a : - Π (A : Type) [_inst_1 : has_add A] [_inst_2 : has_zero A] (a : A), +λ (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_zero A] (a : A) +(H : @eq A (@add A _inst_1 a (@zero A _inst_2)) a) [_inst_3 : has_add A] +(H : @eq A a (@add A _inst_3 (@zero A _inst_2) (@zero A _inst_2))), @add A _inst_3 a a : + Π (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_zero A] (a : A), @eq A (@add A _inst_1 a (@zero A _inst_2)) a → Π [_inst_3 : has_add A], @eq A a (@add A _inst_3 (@zero A _inst_2) (@zero A _inst_2)) → A λ (a b : nat) (H : @gt nat nat.nat_has_lt a b) [_inst_4 : has_lt nat], @lt nat _inst_4 a b : diff --git a/tests/lean/eta_bug.lean.expected.out b/tests/lean/eta_bug.lean.expected.out index 6ce8ac64d8..971634a46d 100644 --- a/tests/lean/eta_bug.lean.expected.out +++ b/tests/lean/eta_bug.lean.expected.out @@ -1 +1 @@ -λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.rec H₁ H₂ +λ (A : Type u_1) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.rec H₁ H₂ diff --git a/tests/lean/eta_tac.lean.expected.out b/tests/lean/eta_tac.lean.expected.out index a2cb3e98b2..a1e65920a3 100644 --- a/tests/lean/eta_tac.lean.expected.out +++ b/tests/lean/eta_tac.lean.expected.out @@ -1,4 +1,4 @@ -λ {A : Type} [_inst_1 : has_add A] (a a_1 : A), @add A _inst_1 a a_1 +λ {A : Type ?} [_inst_1 : has_add A] (a a_1 : A), @add A _inst_1 a a_1 λ (a : nat), nat.succ a λ (a_1 : nat), @add nat nat_has_add a a_1 λ (x a : nat), @add nat nat_has_add x a diff --git a/tests/lean/ftree.lean.expected.out b/tests/lean/ftree.lean.expected.out index a3fc5d88b5..6f46e44467 100644 --- a/tests/lean/ftree.lean.expected.out +++ b/tests/lean/ftree.lean.expected.out @@ -1,2 +1,2 @@ -ftree.{l_1 l_2} : Type.{l_1} → Type.{l_2} → Type.{max 1 l_1 l_2} -ftree.{l_1 l_2} : Type.{l_1} → Type.{l_2} → Type.{max 1 l_1 l_2} +ftree : Type → Type → Type +ftree : Type → Type → Type diff --git a/tests/lean/inaccessible.lean b/tests/lean/inaccessible.lean index 3ff7e51c00..146fdaea7f 100644 --- a/tests/lean/inaccessible.lean +++ b/tests/lean/inaccessible.lean @@ -1,5 +1,5 @@ universe variables u v -inductive imf {A : Type u} {B : Type v} (f : A → B) : B → Type +inductive imf {A : Type u} {B : Type v} (f : A → B) : B → Type (max 1 u v) | mk : ∀ (a : A), imf (f a) definition inv_1 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A diff --git a/tests/lean/inaccessible2.lean b/tests/lean/inaccessible2.lean index 498ff92987..aed7ce1efc 100644 --- a/tests/lean/inaccessible2.lean +++ b/tests/lean/inaccessible2.lean @@ -1,6 +1,6 @@ set_option new_elaborator true -inductive imf {A B : Type*} (f : A → B) : B → Type +inductive imf {A B : Type*} (f : A → B) : B → Type* | mk : ∀ (a : A), imf (f a) definition inv_1 {A B : Type*} (f : A → B) : ∀ (b : B), imf f b → A diff --git a/tests/lean/instance_cache1.lean.expected.out b/tests/lean/instance_cache1.lean.expected.out index 0389542f5a..26248627e4 100644 --- a/tests/lean/instance_cache1.lean.expected.out +++ b/tests/lean/instance_cache1.lean.expected.out @@ -1,15 +1,15 @@ instance_cache1.lean:5:2: error: failed to synthesize type class instance for -A : Type, +A : Type ?, a : A, this : has_add A ⊢ has_add A instance_cache1.lean:8:7: error: failed to synthesize type class instance for -A : Type, +A : Type ?, a : A, s : has_add A ⊢ has_add A instance_cache1.lean:11:19: error: failed to synthesize type class instance for -A : Type, +A : Type ?, a : A, s : has_add A ⊢ has_add A diff --git a/tests/lean/instance_cache_bug1.lean b/tests/lean/instance_cache_bug1.lean index c75c7716fc..3c7df9b31c 100644 --- a/tests/lean/instance_cache_bug1.lean +++ b/tests/lean/instance_cache_bug1.lean @@ -1,4 +1,4 @@ -constant A : Type₁ +constant A : Type constant a : A constant A_has_add : has_add A diff --git a/tests/lean/nary_overload.lean.expected.out b/tests/lean/nary_overload.lean.expected.out index b07a023082..818f28afcb 100644 --- a/tests/lean/nary_overload.lean.expected.out +++ b/tests/lean/nary_overload.lean.expected.out @@ -3,5 +3,5 @@ nary_overload.lean:16:6: error: ambiguous overload, possible interpretations [a, b, c] [a, b, c] : vec A [a, b, c] : lst A -@vec.cons.{1} A a (@vec.cons.{1} A b (@vec.cons.{1} A c (@vec.nil.{1} A))) : vec.{1} A -@lst.cons.{1} A a (@lst.cons.{1} A b (@lst.cons.{1} A c (@lst.nil.{1} A))) : lst.{1} A +@vec.cons A a (@vec.cons A b (@vec.cons A c (@vec.nil A))) : vec.{1} A +@lst.cons A a (@lst.cons A b (@lst.cons A c (@lst.nil A))) : lst.{1} A diff --git a/tests/lean/no_confusion_type.lean b/tests/lean/no_confusion_type.lean index ea87d426dc..8ebeae044d 100644 --- a/tests/lean/no_confusion_type.lean +++ b/tests/lean/no_confusion_type.lean @@ -8,5 +8,5 @@ inductive vector (A : Type) : nat → Type check vector.no_confusion_type constants a1 a2 : num constants v1 v2 : vector num 2 -constant P : Type₁ +constant P : Type eval vector.no_confusion_type P (vector.vcons a1 v1) (vector.vcons a2 v2) diff --git a/tests/lean/no_confusion_type.lean.expected.out b/tests/lean/no_confusion_type.lean.expected.out index 8792a2bc73..6177c6161f 100644 --- a/tests/lean/no_confusion_type.lean.expected.out +++ b/tests/lean/no_confusion_type.lean.expected.out @@ -1,2 +1,2 @@ -vector.no_confusion_type : Type → vector ?M_1 ?M_2 → vector ?M_1 ?M_2 → Type +vector.no_confusion_type : Type u_1 → vector ?M_1 ?M_2 → vector ?M_1 ?M_2 → Type u_1 (2 = 2 → a1 = a2 → v1 == v2 → P) → P diff --git a/tests/lean/notation.lean b/tests/lean/notation.lean index 2611c923ca..97e3b56d5b 100644 --- a/tests/lean/notation.lean +++ b/tests/lean/notation.lean @@ -10,7 +10,7 @@ check (1:num) = (2 + 3)*2 check (2:num) + 3 * 2 = 3 * 2 + 2 check (true ∨ false) = (true ∨ false) ∧ true check true ∧ (false ∨ true) -constant A : Type₁ +constant A : Type constant a : A notation 1 := a check a diff --git a/tests/lean/notation.lean.expected.out b/tests/lean/notation.lean.expected.out index 81c54d25b3..eb4746727c 100644 --- a/tests/lean/notation.lean.expected.out +++ b/tests/lean/notation.lean.expected.out @@ -8,4 +8,4 @@ true ∧ false ∧ true : Prop (true ∨ false) = (true ∨ false) ∧ true : Prop true ∧ (false ∨ true) : Prop 1 : A -ℕ → ℕ : Type₁ +ℕ → ℕ : Type diff --git a/tests/lean/notation4.lean b/tests/lean/notation4.lean index d4d08d2c6b..41c90e4df2 100644 --- a/tests/lean/notation4.lean +++ b/tests/lean/notation4.lean @@ -1,7 +1,7 @@ -- open sigma inductive List (T : Type) : Type | nil {} : List | cons : T → List → List 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 +check ∃ (A : Type) (x y : A), x = y check ∃ (x : num), x = 0 check Σ (x : num), x = 10 -check Σ (A : Type₁), List A +check Σ (A : Type), List A diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out index 8f564d9e20..08bf2b3a64 100644 --- a/tests/lean/notation4.lean.expected.out +++ b/tests/lean/notation4.lean.expected.out @@ -1,4 +1,4 @@ -∃ (A : Type₁) (x y : A), x = y : Prop +∃ (A : Type) (x y : A), x = y : Prop ∃ (x : num), x = 0 : Prop -Σ (x : num), x = 10 : Type₁ -Σ (A : Type₁), List A : Type₂ +Σ (x : num), x = 10 : Type +Σ (A : Type), List A : Type₂ diff --git a/tests/lean/param_binder_update.lean b/tests/lean/param_binder_update.lean index d1a9057609..bc58d874d8 100644 --- a/tests/lean/param_binder_update.lean +++ b/tests/lean/param_binder_update.lean @@ -1,5 +1,5 @@ section - parameter {A : Type} + parameter {A : Type*} parameter A @@ -14,7 +14,7 @@ check @id check @id₂ section - parameters {A : Type} {B : Type} + parameters {A : Type*} {B : Type*} definition foo1 (a : A) (b : B) := a @@ -42,7 +42,7 @@ check @foo3 check @foo4 section - variables {A : Type} {B : Type} + variables {A : Type*} {B : Type*} definition boo1 (a : A) (b : B) := a @@ -65,7 +65,7 @@ section end section - variables {A : Type} {B : Type} + variables {A : Type*} {B : Type*} parameter (A) -- ERROR variable (C) -- ERROR diff --git a/tests/lean/param_binder_update.lean.expected.out b/tests/lean/param_binder_update.lean.expected.out index 0e1e631150..f2ba87bc89 100644 --- a/tests/lean/param_binder_update.lean.expected.out +++ b/tests/lean/param_binder_update.lean.expected.out @@ -1,17 +1,17 @@ -id : Π {A : Type}, A → A -id₂ : Π {A : Type}, A → A +id : Π {A : Type u_1}, A → A +id₂ : Π {A : Type u_1}, A → A foo1 : A → B → A foo2 : A → B → A foo3 : A → B → A foo4 : A → B → A -foo1 : Π {A : Type} {B : Type}, A → B → A -foo2 : Π {A : Type} (B : Type), A → B → A -foo3 : Π (A : Type) {B : Type}, A → B → A -foo4 : Π (A : Type) (B : Type), A → B → A -boo1 : Π {A : Type} {B : Type}, A → B → A -boo2 : Π {A : Type} (B : Type), A → B → A -boo3 : Π (A : Type) {B : Type}, A → B → A -boo4 : Π (A : Type) (B : Type), A → B → A +foo1 : Π {A : Type u_1} {B : Type u_2}, A → B → A +foo2 : Π {A : Type u_1} (B : Type u_2), A → B → A +foo3 : Π (A : Type u_1) {B : Type u_2}, A → B → A +foo4 : Π (A : Type u_1) (B : Type u_2), A → B → A +boo1 : Π {A : Type u_1} {B : Type u_2}, A → B → A +boo2 : Π {A : Type u_1} (B : Type u_2), A → B → A +boo3 : Π (A : Type u_1) {B : Type u_2}, A → B → A +boo4 : Π (A : Type u_1) (B : Type u_2), A → B → A param_binder_update.lean:70:12: error: invalid parameter binder type update, 'A' is a variable param_binder_update.lean:71:11: error: invalid variable binder type update, 'C' is not a variable param_binder_update.lean:72:12: error: invalid variable binder type update, 'C' is not a variable diff --git a/tests/lean/param_binder_update2.lean b/tests/lean/param_binder_update2.lean index 862c293e9b..2ed26cc919 100644 --- a/tests/lean/param_binder_update2.lean +++ b/tests/lean/param_binder_update2.lean @@ -1,5 +1,5 @@ section - parameters {A : Type} {B : Type} + parameters {A : Type*} {B : Type*} definition foo1 (a : A) (b : B) := a diff --git a/tests/lean/param_binder_update2.lean.expected.out b/tests/lean/param_binder_update2.lean.expected.out index b5b750ee77..d7c93c24be 100644 --- a/tests/lean/param_binder_update2.lean.expected.out +++ b/tests/lean/param_binder_update2.lean.expected.out @@ -1,4 +1,4 @@ -foo1 : Π {A : Type} {B : Type}, A → B → A -foo2 : Π {A : Type} (B : Type), A → B → A -foo3 : Π (A : Type) {B : Type}, A → B → A -foo4 : Π (A : Type) (B : Type), A → B → A +foo1 : Π {A : Type u_1} {B : Type u_2}, A → B → A +foo2 : Π {A : Type u_1} (B : Type u_2), A → B → A +foo3 : Π (A : Type u_1) {B : Type u_2}, A → B → A +foo4 : Π (A : Type u_1) (B : Type u_2), A → B → A diff --git a/tests/lean/parsing_only.lean.expected.out b/tests/lean/parsing_only.lean.expected.out index 825a48b2ad..189fd382b2 100644 --- a/tests/lean/parsing_only.lean.expected.out +++ b/tests/lean/parsing_only.lean.expected.out @@ -1,3 +1,3 @@ 10+++ : num g 10 : num -Type : Type +Type 8 : Type 9 diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out index 6825b973a5..d908942421 100644 --- a/tests/lean/print_ax1.lean.expected.out +++ b/tests/lean/print_ax1.lean.expected.out @@ -1,3 +1,3 @@ -quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ -classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} +quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ +classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} propext : ∀ {a b : Prop}, (a ↔ b) → a = b diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out index 6825b973a5..d908942421 100644 --- a/tests/lean/print_ax2.lean.expected.out +++ b/tests/lean/print_ax2.lean.expected.out @@ -1,3 +1,3 @@ -quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ -classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} +quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ +classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} propext : ∀ {a b : Prop}, (a ↔ b) → a = b diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out index d05249b660..1238f47ae7 100644 --- a/tests/lean/print_ax3.lean.expected.out +++ b/tests/lean/print_ax3.lean.expected.out @@ -1,7 +1,7 @@ no axioms ------ -quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ -classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} +quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ +classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} propext : ∀ {a b : Prop}, (a ↔ b) → a = b ------ theorem foo3 : 0 = 0 := diff --git a/tests/lean/private_structure.lean.expected.out b/tests/lean/private_structure.lean.expected.out index 1e2c121f5c..023fe970ea 100644 --- a/tests/lean/private_structure.lean.expected.out +++ b/tests/lean/private_structure.lean.expected.out @@ -1,5 +1,5 @@ -bla : Type₁ -point : Type₁ +bla : Type +point : Type point.mk : ℕ → ℕ → point point.rec : (Π (x y : ℕ), ?M_1 (point.mk x y)) → Π (n : point), ?M_1 n point.rec_on : Π (n : point), (Π (x y : ℕ), ?M_1 (point.mk x y)) → ?M_1 n @@ -7,7 +7,7 @@ point.cases_on : Π (n : point), (Π (x y : ℕ), ?M_1 (point.mk x y)) → ?M_1 point.induction_on : ∀ (n : point), (∀ (x y : ℕ), ?M_1 (point.mk x y)) → ?M_1 n point.x : point → ℕ point.y : point → ℕ -bla : Type₁ +bla : Type private_structure.lean:24:6: error: unknown identifier 'point' private_structure.lean:25:6: error: unknown identifier 'point.mk' private_structure.lean:26:6: error: unknown identifier 'point.rec' @@ -17,7 +17,7 @@ private_structure.lean:29:6: error: unknown identifier 'point.induction_on' private_structure.lean:30:6: error: unknown identifier 'point.no_confusion' private_structure.lean:31:6: error: unknown identifier 'point.x' private_structure.lean:32:6: error: unknown identifier 'point.y' -definition foo.bla : Type.{1} := +definition foo.bla : Type := point private_structure.lean:37:7: error: invalid constructor ⟨...⟩, type is a private inductive datatype foo.mk : foo.bla diff --git a/tests/lean/prodtst.lean.expected.out b/tests/lean/prodtst.lean.expected.out index 47893064a4..d36fd8acc8 100644 --- a/tests/lean/prodtst.lean.expected.out +++ b/tests/lean/prodtst.lean.expected.out @@ -1 +1 @@ -prod2.{l_1 l_2} : Type.{l_1+1} → Type.{l_2+1} → Type.{max (l_1+1) (l_2+1)} +prod2.{u_1 u_2} : Type (u_1+1) → Type (u_2+1) → Type (max (u_1+1) (u_2+1)) diff --git a/tests/lean/restrict_bug.lean.expected.out b/tests/lean/restrict_bug.lean.expected.out index ca680a254a..20ffac966f 100644 --- a/tests/lean/restrict_bug.lean.expected.out +++ b/tests/lean/restrict_bug.lean.expected.out @@ -1 +1 @@ -∀ (a : A) (l : list.{l_1} A), @all.{l_1} A l (R a) : Prop +∀ (a : A) (l : list.{1} A), @all A l (R a) : Prop diff --git a/tests/lean/run/apply4.lean b/tests/lean/run/apply4.lean index c49b5914aa..0b4f00ac63 100644 --- a/tests/lean/run/apply4.lean +++ b/tests/lean/run/apply4.lean @@ -1,6 +1,6 @@ open tactic bool - -constant foo {A : Type} [inhabited A] (a b : A) : a = default A → a = b +universe variables u +constant foo {A : Type u} [inhabited A] (a b : A) : a = default A → a = b example (a b : nat) : a = 0 → a = b := by do diff --git a/tests/lean/run/atomic2.lean b/tests/lean/run/atomic2.lean index 62b26c5a3f..e994136f21 100644 --- a/tests/lean/run/atomic2.lean +++ b/tests/lean/run/atomic2.lean @@ -1,3 +1,3 @@ notation `foo` := Type.{1} -constant f : Type → Type +constant f : Type* → Type* check foo → f foo → foo diff --git a/tests/lean/run/back_chaining3.lean b/tests/lean/run/back_chaining3.lean index 0a2b24ad71..de9215cad0 100644 --- a/tests/lean/run/back_chaining3.lean +++ b/tests/lean/run/back_chaining3.lean @@ -1,7 +1,7 @@ namespace ex open tactic -constant typ : Type₁ +constant typ : Type constant subtype : typ → typ → Prop diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean index 83a213c41f..d3fe7e279e 100644 --- a/tests/lean/run/basic.lean +++ b/tests/lean/run/basic.lean @@ -3,7 +3,7 @@ set_option new_elaborator true constant {l1 l2} A : Type l1 → Type l2 check A -definition {l} tst (A : Type) (B : Type) (C : Type l) : Type := A → B → C +definition {l} tst (A : Type*) (B : Type*) (C : Type l) : Type* := A → B → C check tst constant {l} group : Type (l+1) constant {l} carrier : group.{l} → Type l @@ -12,7 +12,7 @@ noncomputable definition to_carrier (g : group) := carrier g check to_carrier.{1} section - variable A : Type + variable A : Type* check A definition B := A → A end @@ -24,8 +24,8 @@ constant a : N check f a section - variable T1 : Type - variable T2 : Type + variable T1 : Type* + variable T2 : Type* variable f : T1 → T2 → T2 definition double (a : T1) (b : T2) := f a (f a b) end @@ -34,7 +34,7 @@ check double check double.{1 2} definition Prop := Type 0 -constant eq : Π {A : Type}, A → A → Prop +constant eq : Π {A : Type*}, A → A → Prop infix `=`:50 := eq check eq.{1} @@ -55,8 +55,8 @@ check @is_proj3.{1 2} namespace foo section - variables {T1 T2 : Type} - variable {T3 : Type} + variables {T1 T2 : Type*} + variable {T3 : Type*} variable f : T1 → T2 → T2 noncomputable definition is_proj2 := ∀ x y, f x y = y noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z @@ -67,9 +67,9 @@ end foo namespace bla section - variable {T1 : Type} - variable {T2 : Type} - variable {T3 : Type} + variable {T1 : Type*} + variable {T2 : Type*} + variable {T3 : Type*} variable f : T1 → T2 → T2 noncomputable definition is_proj2 := ∀ x y, f x y = y noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z diff --git a/tests/lean/run/confuse_ind.lean b/tests/lean/run/confuse_ind.lean index 49683e9b90..38617d9b84 100644 --- a/tests/lean/run/confuse_ind.lean +++ b/tests/lean/run/confuse_ind.lean @@ -1,4 +1,4 @@ -attribute [reducible] definition mk_arrow (A : Type) (B : Type) := +attribute [reducible] definition mk_arrow (A : Type*) (B : Type*) := A → A → B inductive confuse (A : Type) diff --git a/tests/lean/run/def_brec_reflexive.lean b/tests/lean/run/def_brec_reflexive.lean index 5ff483a334..16bda5b8c1 100644 --- a/tests/lean/run/def_brec_reflexive.lean +++ b/tests/lean/run/def_brec_reflexive.lean @@ -1,6 +1,6 @@ set_option new_elaborator true -inductive inftree (A : Type) +inductive inftree (A : Type*) | leaf : A → inftree | node : (nat → inftree) → inftree diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean index 5655842426..092aedece4 100644 --- a/tests/lean/run/e15.lean +++ b/tests/lean/run/e15.lean @@ -4,7 +4,7 @@ inductive nat : Type | succ : nat → nat namespace nat end nat open nat -inductive list (A : Type) : Type +inductive list (A : Type*) | nil {} : list | cons : A → list → list namespace list end list open list @@ -15,7 +15,7 @@ check @nil nat check cons zero nil -inductive vector (A : Type) : nat → Type +inductive vector (A : Type*) : nat → Type* | vnil {} : vector zero | vcons : forall {n : nat}, A → vector n → vector (succ n) namespace vector end vector open vector @@ -25,6 +25,3 @@ constant n : nat check vcons n vnil check vector.rec - -definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A -:= vector.rec nil (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean index 440ef06ad0..84a112a815 100644 --- a/tests/lean/run/e16.lean +++ b/tests/lean/run/e16.lean @@ -4,7 +4,7 @@ inductive nat : Type | succ : nat → nat namespace nat end nat open nat -inductive list (A : Type) : Type +inductive list (A : Type*) : Type* | nil {} : list | cons : A → list → list namespace list end list open list @@ -16,7 +16,7 @@ check @nil nat check cons zero nil -inductive vector (A : Type) : nat → Type +inductive vector (A : Type*) : nat → Type* | vnil {} : vector zero | vcons : forall {n : nat}, A → vector n → vector (succ n) namespace vector end vector open vector @@ -26,6 +26,3 @@ constant n : nat check vcons n vnil check vector.rec - -definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A -:= vector.rec nil (fun n a v l, cons a l) v diff --git a/tests/lean/run/elab3.lean b/tests/lean/run/elab3.lean index 736afa6006..9a5eb5ce8c 100644 --- a/tests/lean/run/elab3.lean +++ b/tests/lean/run/elab3.lean @@ -1,3 +1,3 @@ set_option pp.binder_types true -axiom Sorry {A : Type} : A +axiom Sorry {A : Type*} : A check (Sorry : ∀ a, a > 0) diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index 63d0009053..4c153525e3 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -1,5 +1,5 @@ section - variable {A : Type} + variable {A : Type*} variable f : A → A → A variable one : A variable inv : A → A @@ -10,22 +10,22 @@ section definition is_inv := ∀ a, a*a^-1 = one end -inductive [class] group_struct (A : Type) : Type +inductive [class] group_struct (A : Type*) : Type* | mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct -inductive group : Type -| mk_group : Π (A : Type), group_struct A → group +inductive group : Type* +| mk_group : Π (A : Type*), group_struct A → group -definition carrier (g : group) : Type +definition carrier (g : group) : Type* := group.rec (λ c s, c) g attribute [instance] definition group_to_struct (g : group) : group_struct (carrier g) -:= group.rec (λ (A : Type) (s : group_struct A), s) g +:= group.rec (λ (A : Type*) (s : group_struct A), s) g check group_struct -definition mul1 {A : Type} {s : group_struct A} (a b : A) : A +definition mul1 {A : Type*} {s : group_struct A} (a b : A) : A := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b infixl `*` := mul1 diff --git a/tests/lean/run/ho.lean b/tests/lean/run/ho.lean index 7119070fb9..d8b6edb42a 100644 --- a/tests/lean/run/ho.lean +++ b/tests/lean/run/ho.lean @@ -1,4 +1,4 @@ -inductive star : Type₁ +inductive star : Type | z : star | s : (nat → star) → star diff --git a/tests/lean/run/ind1.lean b/tests/lean/run/ind1.lean index d8d7c4ee8a..ec18a15967 100644 --- a/tests/lean/run/ind1.lean +++ b/tests/lean/run/ind1.lean @@ -1,4 +1,4 @@ -inductive List (A : Type) : Type +inductive List (A : Type*) : Type* | nil : List | cons : A → List → List namespace List end List open List diff --git a/tests/lean/run/ind2.lean b/tests/lean/run/ind2.lean index f6a95a4d89..a1daa10892 100644 --- a/tests/lean/run/ind2.lean +++ b/tests/lean/run/ind2.lean @@ -4,7 +4,7 @@ inductive nat : Type | succ : nat → nat namespace nat end nat open nat -inductive vector (A : Type) : nat → Type +inductive vector (A : Type*) : nat → Type* | vnil : vector zero | vcons : Π {n : nat}, A → vector n → vector (succ n) namespace vector end vector open vector diff --git a/tests/lean/run/ind7.lean b/tests/lean/run/ind7.lean index 269e55100e..39d9d14366 100644 --- a/tests/lean/run/ind7.lean +++ b/tests/lean/run/ind7.lean @@ -1,5 +1,5 @@ namespace list - inductive list (A : Type) : Type + inductive list (A : Type*) : Type* | nil : list | cons : A → list → list diff --git a/tests/lean/run/indbug2.lean b/tests/lean/run/indbug2.lean index 7978d20627..556d7dc4f9 100644 --- a/tests/lean/run/indbug2.lean +++ b/tests/lean/run/indbug2.lean @@ -1,8 +1,8 @@ set_option pp.implicit true set_option pp.universes true section -parameter {A : Type} -definition foo : A → A → Type := (λ x y, Type) +parameter {A : Type*} +definition foo : A → A → Type* := (λ x y, Type*) inductive bar {a b : A} (f : foo a b) | bar2 : bar end diff --git a/tests/lean/run/inst_bug.lean b/tests/lean/run/inst_bug.lean index c54031faec..efed8ad740 100644 --- a/tests/lean/run/inst_bug.lean +++ b/tests/lean/run/inst_bug.lean @@ -1,5 +1,5 @@ -inductive [class] is_equiv (A B : Type) (f : A → B) : Type -definition inverse (A B : Type) (f : A → B) [H : is_equiv A B f] := Type -definition foo (A : Type) (B : A → Type) (h : A → A) (g : Π(a : A), B a → B a) - [H : Π(a : A), is_equiv _ _ (g a)] (x : A) : Type := +inductive [class] is_equiv (A B : Type*) (f : A → B) : Type* +definition inverse (A B : Type*) (f : A → B) [H : is_equiv A B f] := Type* +definition foo (A : Type*) (B : A → Type*) (h : A → A) (g : Π(a : A), B a → B a) + [H : Π(a : A), is_equiv _ _ (g a)] (x : A) : Type* := inverse (B (h x)) (B (h x)) (g (h x)) diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean index d3f2685ec2..689b730654 100644 --- a/tests/lean/run/interp.lean +++ b/tests/lean/run/interp.lean @@ -9,7 +9,7 @@ inductive univ open univ attribute [reducible] -definition interp : univ → Type₁ +definition interp : univ → Type | ubool := bool | unat := nat | (uarrow fr to) := interp fr → interp to diff --git a/tests/lean/run/match_expr.lean b/tests/lean/run/match_expr.lean index 1d33f37684..c86e784aea 100644 --- a/tests/lean/run/match_expr.lean +++ b/tests/lean/run/match_expr.lean @@ -1,5 +1,5 @@ open tactic -axiom Sorry : ∀ {A:Type}, A +axiom Sorry : ∀ {A:Type*}, A example (a b c : nat) (h₀ : c > 0) (h₁ : a > 1) (h₂ : b > 0) : a + b + c = 0 := by do diff --git a/tests/lean/run/nested_inductive.lean b/tests/lean/run/nested_inductive.lean index a8faa3b870..18eb412fe1 100644 --- a/tests/lean/run/nested_inductive.lean +++ b/tests/lean/run/nested_inductive.lean @@ -1,7 +1,7 @@ set_option trace.inductive_compiler.nested.define.failure true set_option max_memory 1000000 -inductive vec (A : Type) : nat -> Type +inductive vec (A : Type*) : nat -> Type* | vnil : vec 0 | vcons : Pi (n : nat), A -> vec n -> vec (n+1) @@ -14,49 +14,49 @@ end X1 namespace X2 print "with param" -inductive foo (A : Type) +inductive foo (A : Type*) | mk : A -> list foo -> foo end X2 namespace X3 print "with indices" -inductive foo (A B : Type) +inductive foo (A B : Type*) | mk : A -> B -> vec foo 0 -> foo end X3 namespace X4 print "with locals in indices" -inductive foo (A : Type) +inductive foo (A : Type*) | mk : Pi (n : nat), A -> vec foo n -> foo end X4 namespace X5 print "nested-reflexive" -inductive foo (A : Type) +inductive foo (A : Type*) | mk : A -> (Pi (m : nat), vec foo m) -> foo end X5 namespace X6 print "locals + nested-reflexive locals in indices" -inductive foo (A : Type) +inductive foo (A : Type*) | mk : Pi (n : nat), A -> (Pi (m : nat), vec foo (n + m)) -> foo end X6 namespace X7 print "many different nestings" -inductive foo (A : Type) +inductive foo (A : Type*) | mk : Pi (n : nat), A -> list A -> prod A A -> (Pi (m : nat), vec foo (n + m)) -> vec foo n -> foo end X7 namespace X8 print "many different nestings, some sharing" -inductive foo (A : Type) +inductive foo (A : Type*) | mk₁ : Pi (n : nat), A -> (Pi (m : nat), vec (list foo) (n + m)) -> vec foo n -> foo | mk₂ : Pi (n : nat), A -> list A -> prod A A -> (Pi (m : nat), vec foo (n + m)) -> vec foo n -> foo @@ -65,9 +65,9 @@ end X8 namespace X9b print "mutual + nesting" mutual_inductive foo, bar -with foo : Type +with foo : Type* | mk : list (list foo) -> foo -with bar : Type +with bar : Type* | mk : list foo -> bar end X9b @@ -75,13 +75,13 @@ end X9b namespace X10 print "many layers of nesting nested inductive types" -inductive wrap (A : Type) +inductive wrap (A : Type*) | mk : A -> wrap -inductive box (A : Type) +inductive box (A : Type*) | mk : A -> wrap box -> box -inductive foo (A : Type) +inductive foo (A : Type*) | mk : A -> box foo -> foo inductive bar @@ -92,7 +92,7 @@ end X10 namespace X11 print "intro rule that introduces additional nesting" -inductive wrap (A : Type) : Type +inductive wrap (A : Type*) : Type* | mk : list A -> wrap inductive foo @@ -103,10 +103,10 @@ end X11 namespace X12 print "intro rule that introduces a lot of additional nesting" -inductive wrap (A : Type) : Type +inductive wrap (A : Type*) : Type* | mk : list (list A) -> wrap -inductive box (A : Type) +inductive box (A : Type*) | mk : A -> wrap box -> box end X12 @@ -116,12 +116,12 @@ print "with reducible definitions" attribute [reducible] definition list' := @list -inductive wrap (A : Type) : Type +inductive wrap (A : Type*) : Type* | mk : A -> list' A -> wrap attribute [reducible] definition wrap' := @wrap -inductive foo (A : Type) +inductive foo (A : Type*) | mk : A -> wrap' (list' foo) -> foo end X13 diff --git a/tests/lean/run/pack_unpack3.lean b/tests/lean/run/pack_unpack3.lean index 972d0a9a79..377db776a6 100644 --- a/tests/lean/run/pack_unpack3.lean +++ b/tests/lean/run/pack_unpack3.lean @@ -10,7 +10,7 @@ inductive tree (A : Type*) set_option trace.eqn_compiler true -constant P {A : Type*} : tree A → Type₁ +constant P {A : Type*} : tree A → Type constant mk1 {A : Type*} (a : A) : P (tree.leaf a) constant mk2 {A : Type*} (n : nat) (xs : vec (list (list (tree A))) n) : P (tree.node n xs) diff --git a/tests/lean/run/partial_explicit.lean b/tests/lean/run/partial_explicit.lean index 308e205f7a..468f217405 100644 --- a/tests/lean/run/partial_explicit.lean +++ b/tests/lean/run/partial_explicit.lean @@ -8,8 +8,8 @@ example : b + b + a + b = 0 := end section -variables (f : Π {T : Type₁} {a : T} {P : T → Prop}, P a → Π {b : T} {Q : T → Prop}, Q b → Prop) -variables (T : Type₁) (a : T) (P : T → Prop) (pa : P a) +variables (f : Π {T : Type} {a : T} {P : T → Prop}, P a → Π {b : T} {Q : T → Prop}, Q b → Prop) +variables (T : Type) (a : T) (P : T → Prop) (pa : P a) variables (b : T) (Q : T → Prop) (qb : Q b) check @f T a P pa b Q qb -- Prop diff --git a/tests/lean/run/record9.lean b/tests/lean/run/record9.lean index 1b533bd047..3cf0c476dd 100644 --- a/tests/lean/run/record9.lean +++ b/tests/lean/run/record9.lean @@ -1,6 +1,6 @@ -constant fibrant : Type → Prop +constant fibrant : Type* → Prop -structure Fib : Type := -{type : Type} (pred : fibrant type) +structure Fib : Type* := +{type : Type*} (pred : fibrant type) check Fib.mk diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean index 623851345e..dc8e6f6859 100644 --- a/tests/lean/run/simple.lean +++ b/tests/lean/run/simple.lean @@ -1,7 +1,7 @@ prelude definition Prop : Type.{1} := Type.{0} section - parameter A : Type + parameter A : Type* definition eq (a b : A) : Prop := ∀P : A → Prop, P a → P b diff --git a/tests/lean/run/simplifier_canonize_instances.lean b/tests/lean/run/simplifier_canonize_instances.lean index 541ed9bc1a..b92438b330 100644 --- a/tests/lean/run/simplifier_canonize_instances.lean +++ b/tests/lean/run/simplifier_canonize_instances.lean @@ -11,12 +11,12 @@ do (new_target, Heq) ← target >>= simplify failed [], try reflexivity universe l -constants (group : Type → Type.{1}) +constants (group : Type* → Type) attribute group [class] -constants (f₁ : Π (X : Type) (X_grp : group X), X) -constants (f₂ : Π (X : Type) [X_grp : group X], X) -constants (A : Type.{l}) (A_grp₁ : group A) +constants (f₁ : Π (X : Type*) (X_grp : group X), X) +constants (f₂ : Π (X : Type*) [X_grp : group X], X) +constants (A : Type l) (A_grp₁ : group A) attribute [irreducible] noncomputable definition A_grp₂ : group A := A_grp₁ attribute [irreducible] noncomputable definition A_grp₃ (t : true) : group A := A_grp₁ diff --git a/tests/lean/run/simplifier_canonize_subsingletons.lean b/tests/lean/run/simplifier_canonize_subsingletons.lean index eeaa013fe5..10f9ba80db 100644 --- a/tests/lean/run/simplifier_canonize_subsingletons.lean +++ b/tests/lean/run/simplifier_canonize_subsingletons.lean @@ -45,7 +45,7 @@ namespace lambda universe variable l constants (ss : Π {A : Type.{l}}, A → Type.{l}) - [ss_ss : ∀ (T : Type) (t : T), subsingleton (ss t)] + [ss_ss : ∀ (T : Type*) (t : T), subsingleton (ss t)] (A : Type.{l}) (a : A) (ss₁ ss₂ : ss a) @@ -62,7 +62,7 @@ namespace dont_crash_when_locals_incompatible universe variable l constants (ss : Π {A : Type.{l}}, A → Type.{l}) - [ss_ss : ∀ (T : Type) (t : T), subsingleton (ss t)] + [ss_ss : ∀ (T : Type*) (t : T), subsingleton (ss t)] (A : Type.{l}) (a : A) (ss₁ ss₂ : ss a) diff --git a/tests/lean/run/struct_bug1.lean b/tests/lean/run/struct_bug1.lean index b2316a988c..ce00ef133d 100644 --- a/tests/lean/run/struct_bug1.lean +++ b/tests/lean/run/struct_bug1.lean @@ -1,15 +1,15 @@ -variable (A : Type) +variable (A : Type*) structure foo (a : A) := (eqpr : a = a) section - parameter (B : Type) + parameter (B : Type*) structure foo2 (b : B) := (eqpr : b = b) check foo2 - definition tst : B → Type₁ := foo2 + definition tst : B → Type := foo2 end diff --git a/tests/lean/run/structure_test.lean b/tests/lean/run/structure_test.lean index 11cd2e4121..02646bce98 100644 --- a/tests/lean/run/structure_test.lean +++ b/tests/lean/run/structure_test.lean @@ -1,4 +1,4 @@ -inductive point (A B : Type) +inductive point (A B : Type*) | mk : Π (x : A) (y : B), point inductive [class] color @@ -17,7 +17,7 @@ section include E -- include Ha - structure point3d_color (B C : Type) (D : B → Type) extends point (foo A) B, sigma D renaming pr1→y pr2→w := + structure point3d_color (B C : Type*) (D : B → Type*) extends point (foo A) B, sigma D renaming pr1→y pr2→w := mk :: (c : color) (H : x == y) check point3d_color.c diff --git a/tests/lean/run/t11.lean b/tests/lean/run/t11.lean index 73dd755d8c..a671f08e72 100644 --- a/tests/lean/run/t11.lean +++ b/tests/lean/run/t11.lean @@ -1,10 +1,10 @@ -constant A : Type.{1} +constant A : Type constants a b c : A constant f : A → A → A check f a b section - parameters A B : Type - parameters {C D : Type} + parameters A B : Type* + parameters {C D : Type*} parameters [e : A] [d : A] check A check B diff --git a/tests/lean/run/t4.lean b/tests/lean/run/t4.lean index 00bc28481e..c96e7c1f89 100644 --- a/tests/lean/run/t4.lean +++ b/tests/lean/run/t4.lean @@ -1,12 +1,13 @@ +set_option new_elaborator true namespace foo - definition f.{l} (A : Type.{l}) : Type.{l} := A + definition {u} f (A : Type u) : Type u := A check f.{1} end foo -constant N : Type.{1} +constant N : Type section - variable A : Type - definition g (a : A) (B : Type) : A := a + variable A : Type* + definition g (a : A) (B : Type*) : A := a check g.{_ 2} end check g.{2 3} diff --git a/tests/lean/run/tc_loop.lean b/tests/lean/run/tc_loop.lean index 555b08c773..95b9df4299 100644 --- a/tests/lean/run/tc_loop.lean +++ b/tests/lean/run/tc_loop.lean @@ -1,8 +1,8 @@ open tactic check (do { trace "foo", trace_state } : tactic unit) -axiom Sorry {A : Type} : A +axiom Sorry {A : Type*} : A check -λ (A : Type) (a b c d : A) (H₁ : a = b) (H₂ : c = b) (H₃ : d = c), +λ (A : Type*) (a b c d : A) (H₁ : a = b) (H₂ : c = b) (H₃ : d = c), have a = c, by do { trace "have-expr...", trace_state, transitivity, assumption, symmetry, assumption }, show a = d, from Sorry diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean index 1adc9436a7..8946c0974b 100644 --- a/tests/lean/run/univ1.lean +++ b/tests/lean/run/univ1.lean @@ -1,6 +1,6 @@ namespace S1 -axiom I : Type -definition F (X : Type) : Type := (X → Prop) → Prop +axiom I : Type* +definition F (X : Type*) : Type* := (X → Prop) → Prop axiom {u} unfoldd : I.{u} → F I.{u} axiom {l} foldd : F I.{l} → I.{l} axiom iso1 : ∀x, foldd (unfoldd x) = x @@ -9,7 +9,7 @@ end S1 namespace S2 universe u axiom I : Type.{u} -definition F (X : Type) : Type := (X → Prop) → Prop +definition F (X : Type*) : Type* := (X → Prop) → Prop axiom unfoldd : I → F I axiom foldd : F I → I axiom iso1 : ∀x, foldd (unfoldd x) = x @@ -18,8 +18,8 @@ end S2 namespace S3 section - hypothesis I : Type - definition F (X : Type) : Type := (X → Prop) → Prop + hypothesis I : Type* + definition F (X : Type*) : Type* := (X → Prop) → Prop hypothesis unfoldd : I → F I hypothesis foldd : F I → I hypothesis iso1 : ∀x, foldd (unfoldd x) = x diff --git a/tests/lean/run/vm_eval1.lean b/tests/lean/run/vm_eval1.lean index e6276b2757..2bf479fd82 100644 --- a/tests/lean/run/vm_eval1.lean +++ b/tests/lean/run/vm_eval1.lean @@ -3,7 +3,7 @@ open bool nat -- set_option trace.compiler.code_gen true attribute [reducible] -definition foo (b : bool) : Type₁ := +definition foo (b : bool) : Type := cond b nat (nat → nat) definition bla (b : bool) : foo b → nat := diff --git a/tests/lean/sec_param_pp.lean b/tests/lean/sec_param_pp.lean index e671ce5b47..6e6b75f822 100644 --- a/tests/lean/sec_param_pp.lean +++ b/tests/lean/sec_param_pp.lean @@ -1,5 +1,5 @@ section - parameters {A : Type} (a : A) + parameters {A : Type*} (a : A) variable f : A → A → A definition id2 : A := a @@ -14,7 +14,7 @@ section check pr f id2 - definition pr2 (B : Type) (b : B) : A := a + definition pr2 (B : Type*) (b : B) : A := a check pr2 num 10 end diff --git a/tests/lean/struct_class.lean b/tests/lean/struct_class.lean index 610e9b0ebc..1cd37eb1ee 100644 --- a/tests/lean/struct_class.lean +++ b/tests/lean/struct_class.lean @@ -1,9 +1,9 @@ -structure [class] point (A : Type) (B : Type) := +structure [class] point (A : Type*) (B : Type*) := mk :: (x : A) (y : B) print classes -structure point2 (A : Type) (B : Type) := +structure point2 (A : Type*) (B : Type*) := mk :: (x : A) (y : B) print classes diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index 8aa067301c..6ae7f6ba01 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -1,74 +1,74 @@ -alternative : (Type → Type) → Type -applicative : (Type → Type) → Type -decidable : Prop → Type₁ -functor : (Type → Type) → Type -has_add : Type → Type -has_andthen : Type → Type -has_append : Type → Type -has_coe : Type → Type → Type -has_coe_t : Type → Type → Type -has_coe_to_fun : Type → Type -has_coe_to_sort : Type → Type -has_div : Type → Type -has_dvd : Type → Type -has_inv : Type → Type -has_le : Type → Type -has_lift : Type → Type → Type -has_lift_t : Type → Type → Type -has_lt : Type → Type -has_mod : Type → Type -has_mul : Type → Type -has_neg : Type → Type -has_one : Type → Type +alternative : (Type → Type) → Type₂ +applicative : (Type → Type) → Type₂ +decidable : Prop → Type +functor : (Type → Type) → Type₂ +has_add : Type u → Type (max 1 u) +has_andthen : Type u → Type (max 1 u) +has_append : Type u → Type (max 1 u) +has_coe : Type u → Type v → Type (max 1 (imax u v)) +has_coe_t : Type u → Type v → Type (max 1 (imax u v)) +has_coe_to_fun : Type u → Type (max (imax u v) (v+1)) +has_coe_to_sort : Type u → Type (max (imax u v) (v+1)) +has_div : Type u → Type (max 1 u) +has_dvd : Type u → Type (max 1 u) +has_inv : Type u → Type (max 1 u) +has_le : Type u → Type (max 1 u) +has_lift : Type u → Type v → Type (max 1 (imax u v)) +has_lift_t : Type u → Type v → Type (max 1 (imax u v)) +has_lt : Type u → Type (max 1 u) +has_mod : Type u → Type (max 1 u) +has_mul : Type u → Type (max 1 u) +has_neg : Type u → Type (max 1 u) +has_one : Type u → Type (max 1 u) has_ordering : Type → Type -has_sizeof : Type → Type -has_sub : Type → Type -has_to_format : Type → Type -has_to_pexpr : Type → Type -has_to_string : Type → Type +has_sizeof : Type u → Type (max 1 u) +has_sub : Type u → Type (max 1 u) +has_to_format : Type u → Type (max 1 u) +has_to_pexpr : Type u → Type (max 1 u) +has_to_string : Type u → Type (max 1 u) has_to_tactic_format : Type → Type -has_zero : Type → Type -inhabited : Type → Type -is_associative : Π {A : Type}, (A → A → A) → Type₁ -monad : (Type → Type) → Type -nonempty : Type → Prop -point : Type → Type → Type -setoid : Type → Type -subsingleton : Type → Prop -alternative : (Type → Type) → Type -applicative : (Type → Type) → Type -decidable : Prop → Type₁ -functor : (Type → Type) → Type -has_add : Type → Type -has_andthen : Type → Type -has_append : Type → Type -has_coe : Type → Type → Type -has_coe_t : Type → Type → Type -has_coe_to_fun : Type → Type -has_coe_to_sort : Type → Type -has_div : Type → Type -has_dvd : Type → Type -has_inv : Type → Type -has_le : Type → Type -has_lift : Type → Type → Type -has_lift_t : Type → Type → Type -has_lt : Type → Type -has_mod : Type → Type -has_mul : Type → Type -has_neg : Type → Type -has_one : Type → Type +has_zero : Type u → Type (max 1 u) +inhabited : Type u → Type (max 1 u) +is_associative : Π {A : Type u}, (A → A → A) → Type +monad : (Type → Type) → Type₂ +nonempty : Type u → Prop +point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2) +setoid : Type u → Type (max 1 u) +subsingleton : Type u → Prop +alternative : (Type → Type) → Type₂ +applicative : (Type → Type) → Type₂ +decidable : Prop → Type +functor : (Type → Type) → Type₂ +has_add : Type u → Type (max 1 u) +has_andthen : Type u → Type (max 1 u) +has_append : Type u → Type (max 1 u) +has_coe : Type u → Type v → Type (max 1 (imax u v)) +has_coe_t : Type u → Type v → Type (max 1 (imax u v)) +has_coe_to_fun : Type u → Type (max (imax u v) (v+1)) +has_coe_to_sort : Type u → Type (max (imax u v) (v+1)) +has_div : Type u → Type (max 1 u) +has_dvd : Type u → Type (max 1 u) +has_inv : Type u → Type (max 1 u) +has_le : Type u → Type (max 1 u) +has_lift : Type u → Type v → Type (max 1 (imax u v)) +has_lift_t : Type u → Type v → Type (max 1 (imax u v)) +has_lt : Type u → Type (max 1 u) +has_mod : Type u → Type (max 1 u) +has_mul : Type u → Type (max 1 u) +has_neg : Type u → Type (max 1 u) +has_one : Type u → Type (max 1 u) has_ordering : Type → Type -has_sizeof : Type → Type -has_sub : Type → Type -has_to_format : Type → Type -has_to_pexpr : Type → Type -has_to_string : Type → Type +has_sizeof : Type u → Type (max 1 u) +has_sub : Type u → Type (max 1 u) +has_to_format : Type u → Type (max 1 u) +has_to_pexpr : Type u → Type (max 1 u) +has_to_string : Type u → Type (max 1 u) has_to_tactic_format : Type → Type -has_zero : Type → Type -inhabited : Type → Type -is_associative : Π {A : Type}, (A → A → A) → Type₁ -monad : (Type → Type) → Type -nonempty : Type → Prop -point : Type → Type → Type -setoid : Type → Type -subsingleton : Type → Prop +has_zero : Type u → Type (max 1 u) +inhabited : Type u → Type (max 1 u) +is_associative : Π {A : Type u}, (A → A → A) → Type +monad : (Type → Type) → Type₂ +nonempty : Type u → Prop +point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2) +setoid : Type u → Type (max 1 u) +subsingleton : Type u → Prop diff --git a/tests/lean/subpp.lean.expected.out b/tests/lean/subpp.lean.expected.out index 28e6e568c9..e754354b5c 100644 --- a/tests/lean/subpp.lean.expected.out +++ b/tests/lean/subpp.lean.expected.out @@ -1 +1 @@ -{x : ℕ \ x > 0} : Type₁ +{x : ℕ \ x > 0} : Type diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out index f65c00e510..8b50feb54d 100644 --- a/tests/lean/t3.lean.expected.out +++ b/tests/lean/t3.lean.expected.out @@ -1,15 +1,15 @@ -Type -Type -Type -Type +Type u +Type tst.v +Type tst.v +Type tst.v t3.lean:9:16: error: unknown universe 'v' -Type +Type z t3.lean:14:16: error: unknown universe 'z' t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section -Type -Type -Type -Type -Type +Type tst.v +Type u +Type tst.foo.U +Type tst.v +Type tst.foo.U t3.lean:33:2: error: universe level alias 'u' shadows existing global universe level t3.lean:35:16: error: unknown universe 'bla.u' diff --git a/tests/lean/t6.lean b/tests/lean/t6.lean index 12e3537794..2729808e0a 100644 --- a/tests/lean/t6.lean +++ b/tests/lean/t6.lean @@ -1,6 +1,6 @@ prelude definition Prop : Type.{1} := Type.{0} section - variable {A : Type} -- Mark A as implicit parameter + variable {A : Type*} -- Mark A as implicit parameter variable R : A → A → Prop definition id (a : A) : A := a definition refl : Prop := forall (a : A), R a a diff --git a/tests/lean/tactic_failure.lean.expected.out b/tests/lean/tactic_failure.lean.expected.out index ae55b99fb7..a8e80e2474 100644 --- a/tests/lean/tactic_failure.lean.expected.out +++ b/tests/lean/tactic_failure.lean.expected.out @@ -1,7 +1,6 @@ tactic_failure.lean:4:0: error: assumption tactic failed state: -A : Type, -B : Type, +A B : Type, Hb : B ⊢ A tactic_failure.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables diff --git a/tests/lean/tuple.lean b/tests/lean/tuple.lean index b2aa631d20..53c718625d 100644 --- a/tests/lean/tuple.lean +++ b/tests/lean/tuple.lean @@ -3,7 +3,7 @@ open nat prod set_option pp.universes true -definition tuple (A : Type) (n : nat) : Type := +definition tuple (A : Type*) (n : nat) : Type* := nat.rec_on n A (λ n r, r × A) check @tuple diff --git a/tests/lean/tuple.lean.expected.out b/tests/lean/tuple.lean.expected.out index f598af3c4b..973ad13c73 100644 --- a/tests/lean/tuple.lean.expected.out +++ b/tests/lean/tuple.lean.expected.out @@ -1 +1 @@ -tuple.{l_1} : Type.{max 1 l_1} → ℕ → Type.{max 1 l_1} +tuple.{u_1} : Type (max 1 u_1) → ℕ → Type (max 1 u_1) diff --git a/tests/lean/type_class_bug.lean.expected.out b/tests/lean/type_class_bug.lean.expected.out index 66757ef628..e8af6f8b3a 100644 --- a/tests/lean/type_class_bug.lean.expected.out +++ b/tests/lean/type_class_bug.lean.expected.out @@ -1,14 +1,14 @@ -@monad.bind.{1 1} list.{1} list_is_monad.{1} nat nat (@list.cons.{1} nat (@one.{1} nat nat_has_one) (@list.nil.{1} nat)) - (λ (a : nat), @return.{1 1} list.{1} list_is_monad.{1} nat a) : +@monad.bind list.{1} list_is_monad nat nat (@list.cons.{1} nat (@one.{1} nat nat_has_one) (@list.nil.{1} nat)) + (λ (a : nat), @return list.{1} list_is_monad nat a) : list.{1} nat -@monad.bind.{1 1} list.{1} list_is_monad.{1} nat (prod.{1 1} nat nat) +@monad.bind list.{1} list_is_monad nat (prod.{1 1} nat nat) (@list.cons.{1} nat (@one.{1} nat nat_has_one) (@list.cons.{1} nat (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)) (@list.cons.{1} nat (@bit1.{1} nat nat_has_one nat_has_add (@one.{1} nat nat_has_one)) (@list.nil.{1} nat)))) (λ (a : nat), - @monad.bind.{1 1} list.{1} list_is_monad.{1} nat (prod.{1 1} nat nat) + @monad.bind list.{1} list_is_monad nat (prod.{1 1} nat nat) (@list.cons.{1} nat (@bit1.{1} nat nat_has_one nat_has_add (@one.{1} nat nat_has_one)) (@list.cons.{1} nat (@bit0.{1} nat nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one))) (@list.nil.{1} nat))) - (λ (b : nat), @return.{1 1} list.{1} list_is_monad.{1} (prod.{1 1} nat nat) (@prod.mk.{1 1} nat nat a b))) : + (λ (b : nat), @return list.{1} list_is_monad (prod.{1 1} nat nat) (@prod.mk.{1 1} nat nat a b))) : list.{1} (prod.{1 1} nat nat) diff --git a/tests/lean/unification_hints1.lean b/tests/lean/unification_hints1.lean index 4ecb6302aa..9c50d04c88 100644 --- a/tests/lean/unification_hints1.lean +++ b/tests/lean/unification_hints1.lean @@ -1,11 +1,11 @@ -- open list nat -structure unification_constraint := {A : Type} (lhs : A) (rhs : A) +structure unification_constraint := {A : Type*} (lhs : A) (rhs : A) structure unification_hint := (pattern : unification_constraint) (constraints : list unification_constraint) namespace toy -constants (A : Type.{1}) (f h : A → A) (x y z : A) +constants (A : Type) (f h : A → A) (x y z : A) attribute [irreducible] noncomputable definition g (x y : A) : A := f z @@ -37,13 +37,13 @@ end add namespace canonical inductive Canonical -| mk : Π (carrier : Type) (op : carrier → carrier), Canonical +| mk : Π (carrier : Type*) (op : carrier → carrier), Canonical attribute [irreducible] -definition Canonical.carrier (s : Canonical) : Type := +definition Canonical.carrier (s : Canonical) : Type* := Canonical.rec_on s (λ c op, c) -constants (A : Type.{1}) (f : A → A) (x : A) +constants (A : Type) (f : A → A) (x : A) noncomputable definition A_canonical : Canonical := Canonical.mk A f #unify (Canonical.carrier A_canonical), A diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean index 776feb0e2f..95d41ac9b2 100644 --- a/tests/lean/univ.lean +++ b/tests/lean/univ.lean @@ -1,20 +1,20 @@ -- -definition id2 (A : Type) (a : A) := a +definition id2 (A : Type*) (a : A) := a + +check id2 Type* num + +check id2 Type* num -check id2 (Type) num check id2 Type num - -check id2 (Type 1) num - check id2 _ num check id2 (Type (_+1)) num check id2 (Type (0+1)) num -check id2 Type (Type 1) +check id2 Type* (Type 1) -check id2 (Type) (Type 1) +check id2 (Type*) (Type 1) diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out index c59b66dc70..77fec7f613 100644 --- a/tests/lean/univ.lean.expected.out +++ b/tests/lean/univ.lean.expected.out @@ -1,8 +1,8 @@ -id2 Type₁ num : Type₁ -id2 Type₁ num : Type₁ -id2 Type₁ num : Type₁ -id2 Type₁ num : Type₁ -id2 Type₁ num : Type₁ -id2 Type₁ num : Type₁ -id2 Type₂ Type₁ : Type₂ -id2 Type₂ Type₁ : Type₂ +id2 Type num : Type +id2 Type num : Type +id2 Type num : Type +id2 Type num : Type +id2 Type num : Type +id2 Type num : Type +id2 Type₂ Type : Type₂ +id2 Type₂ Type : Type₂ diff --git a/tests/lean/univ_vars.lean.expected.out b/tests/lean/univ_vars.lean.expected.out index 9c12fc3865..e614f6a58a 100644 --- a/tests/lean/univ_vars.lean.expected.out +++ b/tests/lean/univ_vars.lean.expected.out @@ -1,5 +1,5 @@ -id1 : Π (A : Type.{u}), A → A -id2.{l_2} : Π (B : Type.{l_2}), B → B -id3.{l_2} : Π (C : Type.{l_2}), C → C -foo.{l_2} : Π (A₁ A₂ : Type.{l_2}), A₁ → A₂ → Prop -Type.{m} : Type.{m+1} +id1 : Π (A : Type u), A → A +id2 : Π (B : Type), B → B +id3.{u_1} : Π (C : Type u_1), C → C +foo.{u_1} : Π (A₁ A₂ : Type u_1), A₁ → A₂ → Prop +Type m : Type (m+1) diff --git a/tests/lean/user_attribute.lean.expected.out b/tests/lean/user_attribute.lean.expected.out index 0f3aad5e2b..52a84c3516 100644 --- a/tests/lean/user_attribute.lean.expected.out +++ b/tests/lean/user_attribute.lean.expected.out @@ -1,11 +1,11 @@ eq.refl attribute [foo, refl] -constructor eq.refl : ∀ {A : Type} (a : A), a = a +constructor eq.refl : ∀ {A : Type u} (a : A), a = a [eq.refl] --- eq.refl attribute [foo, foo.baz, refl] -constructor eq.refl : ∀ {A : Type} (a : A), a = a +constructor eq.refl : ∀ {A : Type u} (a : A), a = a [eq.refl] user_attribute.lean:24:0: error: an attribute named [reducible] has already been registered state: diff --git a/tests/lean/var2.lean.expected.out b/tests/lean/var2.lean.expected.out index 4983c8d570..969a5f5c7f 100644 --- a/tests/lean/var2.lean.expected.out +++ b/tests/lean/var2.lean.expected.out @@ -1 +1 @@ -foo : Π (B : Type), B → Π (A : Type), A → A = B → Prop +foo : Π (B : Type u_1), B → Π (A : Type u_1), A → A = B → Prop