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