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

@@ -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

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

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
 

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]

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 :=

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.

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 -/

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

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
 

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.

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

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)

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
 

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

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 :=

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);
     }
 }
 

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<level> m_R; /* map from tagged g_level_prefix to "clean" name not in L. */
     name_map<level> 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<level> {
                 if (is_param(l)) {
                     name const & n = param_id(l);

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<tactic_state> 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;

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));

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))));
     }
 }
 

src/frontends/lean/util.cpp

@@ -416,6 +416,6 @@ pair<name, option_kind> 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()));
 }
 }

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<expr> 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;
         });

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<expr> 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);

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))

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

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

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

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

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

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

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

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

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

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 ?

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)

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)
 

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

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

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

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

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₂

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,

tests/lean/def3.lean.expected.out

@@ -1 +1 @@
-f : Π (A : Type), A → A
+f : Π (A : Type u_1), A → A

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 : ℕ

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

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

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

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

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

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 :

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₂

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

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

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

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

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

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
 

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

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)

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

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

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

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

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₂

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

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

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
 

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

tests/lean/parsing_only.lean.expected.out

@@ -1,3 +1,3 @@
 10+++ : num
 g 10 : num
-Type : Type
+Type 8 : Type 9

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

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

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 :=

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

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))

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

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

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

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
 

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

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)

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
 

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

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

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)

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

tests/lean/run/ho.lean

@@ -1,4 +1,4 @@
-inductive star : Type₁
+inductive star : Type
 | z  : star
 | s  : (nat → star) → star
 

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

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

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
 

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

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))

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

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

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

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)
 

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

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

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

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₁

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)