chore: update stage0

2020-01-05 16:27:05 -08:00 · 2020-01-05 16:27:05 -08:00 · af6f7f4bc8
commit af6f7f4bc8
parent 0231841984
41 changed files with 25914 additions and 7797 deletions
--- a/stage0/src/Init/Data/Array/Basic.lean
+++ b/stage0/src/Init/Data/Array/Basic.lean
@ -588,6 +588,9 @@ eraseIdxSzAux a (i.val + 1) a rfl
 def contains [HasBeq α] (as : Array α) (a : α) : Bool :=
 as.any $ fun b => a == b

+def elem [HasBeq α] (a : α) (as : Array α) : Bool :=
+as.contains a
+
 partial def insertAtAux {α} (i : Nat) : Array α → Nat → Array α
 | as, j =>
  if i == j then as
--- a/stage0/src/Init/Lean/Attributes.lean
+++ b/stage0/src/Init/Lean/Attributes.lean
@ -12,6 +12,14 @@ namespace Lean
 inductive AttributeApplicationTime
 | afterTypeChecking | afterCompilation | beforeElaboration

+def AttributeApplicationTime.beq : AttributeApplicationTime → AttributeApplicationTime → Bool
+| AttributeApplicationTime.afterTypeChecking, AttributeApplicationTime.afterTypeChecking => true
+| AttributeApplicationTime.afterCompilation,  AttributeApplicationTime.afterCompilation  => true
+| AttributeApplicationTime.beforeElaboration, AttributeApplicationTime.beforeElaboration => true
+| _,                                          _                                          => false
+
+instance AttributeApplicationTime.hasBeq : HasBeq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩
+
 -- TODO: after we delete the old frontend, we should use `EIO` with a richer exception kind at AttributeImpl.
 -- We must perform a similar modification at `PersistentEnvExtension`

@ -28,6 +36,11 @@ structure AttributeImpl :=
 (popScope (env : Environment) : IO Environment := pure env)
 (applicationTime := AttributeApplicationTime.afterTypeChecking)

+/- Auxiliary function for parsing attribute arguments -/
+def Syntax.hasArgs : Syntax → Bool
+| Syntax.node _ args => args.size > 0
+| _                  => false
+
 instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
 ⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure env }⟩

@ -165,7 +178,7 @@ let attrImpl : AttributeImpl := {
  name  := name,
  descr := descr,
  add   := fun env decl args persistent => do
-    unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument"));
+    when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument"));
    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
    unless (env.getModuleIdxFor? decl).isNone $
      throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
--- a/stage0/src/Init/Lean/Class.lean
+++ b/stage0/src/Init/Lean/Class.lean
@ -141,7 +141,7 @@ registerAttribute {
  name  := `class,
  descr := "type class",
  add   := fun env decl args persistent => do
-    unless args.isMissing $ throw (IO.userError ("invalid attribute 'class', unexpected argument"));
+    when args.hasArgs $ throw (IO.userError ("invalid attribute 'class', unexpected argument"));
    unless persistent $ throw (IO.userError ("invalid attribute 'class', must be persistent"));
    IO.ofExcept (addClass env decl)
 }
--- a/stage0/src/Init/Lean/Elab/Command.lean
+++ b/stage0/src/Init/Lean/Elab/Command.lean
@ -20,15 +20,16 @@ structure Scope :=
 (opts          : Options := {})
 (currNamespace : Name := Name.anonymous)
 (openDecls     : List OpenDecl := [])
-(univNames     : List Name := [])
+(levelNames    : List Name := [])
 (varDecls      : Array Syntax := #[])

 instance Scope.inhabited : Inhabited Scope := ⟨{ kind := "", header := "" }⟩

 structure State :=
-(env      : Environment)
-(messages : MessageLog := {})
-(scopes   : List Scope := [{ kind := "root", header := "" }])
+(env            : Environment)
+(messages       : MessageLog := {})
+(scopes         : List Scope := [{ kind := "root", header := "" }])
+(nextMacroScope : Nat := 1)

 instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩

@ -36,10 +37,11 @@ def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options :=
 { env := env, messages := messages, scopes := [{ kind := "root", header := "", opts := opts }] }

 structure Context :=
-(fileName : String)
-(fileMap  : FileMap)
-(stateRef : IO.Ref State)
-(cmdPos   : String.Pos := 0)
+(fileName       : String)
+(fileMap        : FileMap)
+(stateRef       : IO.Ref State)
+(cmdPos         : String.Pos := 0)
+(currMacroScope : MacroScope := 0)

 abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
 abbrev CommandElabM := CommandElabCoreM Exception
@ -49,7 +51,7 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit
 mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)

 private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
-mkMessageAux ctx ref ("IO error, " ++ toString err) MessageSeverity.error
+mkMessageAux ctx ref (toString err) MessageSeverity.error

@[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
 EIO.adaptExcept (ioErrorToMessage ctx ref) x
@ -77,6 +79,19 @@ instance CommandElabM.monadLog : MonadLog CommandElabM :=
  getFileName := do ctx ← read; pure ctx.fileName,
  logMessage  := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }

+protected def getCurrMacroScope : CommandElabM Nat := do
+ctx ← read;
+pure ctx.currMacroScope
+
+@[inline] protected def withFreshMacroScope {α} (x : CommandElabM α) : CommandElabM α := do
+fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }));
+adaptReader (fun (ctx : Context) => { ctx with currMacroScope := fresh }) x
+
+instance CommandElabM.MonadQuotation : MonadQuotation CommandElabM := {
+  getCurrMacroScope   := Command.getCurrMacroScope,
+  withFreshMacroScope := @Command.withFreshMacroScope
+}
+
 abbrev CommandElabTable := ElabFnTable CommandElab
 def mkBuiltinCommandElabTable : IO (IO.Ref CommandElabTable) := IO.mkRef {}
@[init mkBuiltinCommandElabTable] constant builtinCommandElabTable : IO.Ref CommandElabTable := arbitrary _
@ -130,36 +145,44 @@ stx.ifNode
    | none      => throwError stx ("command '" ++ toString k ++ "' has not been implemented"))
  (fun _ => throwError stx ("unexpected command"))

+/-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
+def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab :=
+fun stx => do
+  stx ← exp stx.val;
+  elabCommand stx
+
 private def mkTermContext (ctx : Context) (s : State) : Term.Context :=
 let scope := s.scopes.head!;
 { config         := { opts := scope.opts, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
  fileName       := ctx.fileName,
  fileMap        := ctx.fileMap,
  cmdPos         := ctx.cmdPos,
+  currMacroScope := ctx.currMacroScope,
  currNamespace  := scope.currNamespace,
-  univNames      := scope.univNames,
+  levelNames     := scope.levelNames,
  openDecls      := scope.openDecls }

 private def mkTermState (s : State) : Term.State :=
-{ env      := s.env,
-  messages := s.messages }
+{ env            := s.env,
+  messages       := s.messages,
+  nextMacroScope := s.nextMacroScope }

 private def getVarDecls (s : State) : Array Syntax :=
 s.scopes.head!.varDecls

 private def toCommandResult {α} (ctx : Context) (s : State) (result : EStateM.Result Term.Exception Term.State α) : EStateM.Result Exception State α :=
 match result with
-| EStateM.Result.ok a newS                            => EStateM.Result.ok a { env := newS.env, messages := newS.messages, .. s }
-| EStateM.Result.error (Term.Exception.error ex) newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s }
+| EStateM.Result.ok a newS                            => EStateM.Result.ok a { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
+| EStateM.Result.error (Term.Exception.error ex) newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
 | EStateM.Result.error Term.Exception.postpone newS   => unreachable!

 instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
 ⟨throw $ arbitrary _⟩

-@[inline] def runTermElabM {α} (x : TermElabM α) : CommandElabM α := do
+@[inline] def runTermElabM {α} (elab : Array Expr → TermElabM α) : CommandElabM α := do
 ctx ← read;
 s ← get;
-match ((Term.elabBinders (getVarDecls s) (fun _ => x)) (mkTermContext ctx s)).run (mkTermState s) with
+match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s)).run (mkTermState s) with
 | EStateM.Result.ok a newS                            => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
 | EStateM.Result.error (Term.Exception.error ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
 | EStateM.Result.error Term.Exception.postpone newS   => unreachable!
@ -194,24 +217,25 @@ modify $ fun s => {
  scopes := { kind := kind, header := header, currNamespace := newNamespace, .. s.scopes.head! } :: s.scopes,
  .. s }

-private def addScopes (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
+private def addScopes (ref : Syntax) (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
 | Name.anonymous => pure ()
 | Name.str p header _ => do
  addScopes p;
  currNamespace ← getCurrNamespace;
  addScope kind header (if updateNamespace then currNamespace ++ header else currNamespace)
-| _ => unreachable!
+| _ => throwError ref "invalid scope"
+
+private def addNamespace (ref : Syntax) (header : Name) : CommandElabM Unit :=
+addScopes ref "namespace" true header

@[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
-fun n => do
-  let header := n.getIdAt 1;
-  addScopes "namespace" true header
+fun stx => addNamespace stx.val (stx.getIdAt 1)

@[builtinCommandElab «section»] def elabSection : CommandElab :=
-fun n => do
-  let header? := (n.getArg 1).getOptionalIdent?;
+fun stx => do
+  let header? := (stx.getArg 1).getOptionalIdent?;
  match header? with
-  | some header => addScopes "section" false header
+  | some header => addScopes stx.val "section" false header
  | none        => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace

 def getScopes : CommandElabM (List Scope) := do
@ -244,6 +268,12 @@ fun n => do
  | none        => unless (checkAnonymousScope scopes) $ throwError n.val "invalid 'end', name is missing"
  | some header => unless (checkEndHeader header scopes) $ throwError n.val "invalid 'end', name mismatch"

+@[inline] def withNamespace {α} (ref : Syntax) (ns : Name) (elab : CommandElabM α) : CommandElabM α := do
+addNamespace ref ns;
+a ← elab;
+modify $ fun s => { scopes := s.scopes.drop ns.getNumParts, .. s };
+pure a
+
@[specialize] def modifyScope (f : Scope → Scope) : CommandElabM Unit :=
 modify $ fun s =>
  { scopes := match s.scopes with
@ -251,25 +281,28 @@ modify $ fun s =>
    | []   => unreachable!,
    .. s }

-def getUniverseNames : CommandElabM (List Name) := do
-scope ← getScope; pure scope.univNames
+def getLevelNames : CommandElabM (List Name) := do
+scope ← getScope; pure scope.levelNames

-def addUniverse (idStx : Syntax) : CommandElabM Unit := do
+def throwAlreadyDeclaredUniverseLevel {α} (ref : Syntax) (u : Name) : CommandElabM α :=
+throwError ref ("a universe level named '" ++ toString u ++ "' has already been declared")
+
+def addUnivLevel (idStx : Syntax) : CommandElabM Unit := do
 let id := idStx.getId;
-univs ← getUniverseNames;
-if univs.elem id then
-  throwError idStx ("a universe named '" ++ toString id ++ "' has already been declared in this Scope")
+levelNames ← getLevelNames;
+if levelNames.elem id then
+  throwAlreadyDeclaredUniverseLevel idStx id
 else
-  modifyScope $ fun scope => { univNames := id :: scope.univNames, .. scope }
+  modifyScope $ fun scope => { levelNames := id :: scope.levelNames, .. scope }

@[builtinCommandElab «universe»] def elabUniverse : CommandElab :=
 fun n => do
-  addUniverse (n.getArg 1)
+  addUnivLevel (n.getArg 1)

@[builtinCommandElab «universes»] def elabUniverses : CommandElab :=
 fun n => do
  let idsStx := n.getArg 1;
-  idsStx.forArgsM addUniverse
+  idsStx.forArgsM addUnivLevel

@[builtinCommandElab «init_quot»] def elabInitQuot : CommandElab :=
 fun stx => do
@ -395,7 +428,7 @@ fun n => do
  -- `variable` bracktedBinder
  let binder := n.getArg 1;
  -- Try to elaborate `binder` for sanity checking
-  runTermElabM $ Term.elabBinder binder $ fun _ => pure ();
+  runTermElabM $ fun _ => Term.elabBinder binder $ fun _ => pure ();
  modifyScope $ fun scope => { varDecls := scope.varDecls.push binder, .. scope }

@[builtinCommandElab «variables»] def elabVariables : CommandElab :=
@ -403,13 +436,13 @@ fun n => do
  -- `variables` bracktedBinder+
  let binders := (n.getArg 1).getArgs;
  -- Try to elaborate `binders` for sanity checking
-  runTermElabM $ Term.elabBinders binders $ fun _ => pure ();
+  runTermElabM $ fun _ => Term.elabBinders binders $ fun _ => pure ();
  modifyScope $ fun scope => { varDecls := scope.varDecls ++ binders, .. scope }

@[builtinCommandElab «check»] def elabCheck : CommandElab :=
 fun stx => do
  let term := stx.getArg 1;
-  runTermElabM $ do
+  runTermElabM $ fun _ => do
    e    ← Term.elabTerm term none;
    Term.synthesizeSyntheticMVars false;
    type ← Term.inferType stx.val e;
@ -418,6 +451,52 @@ fun stx => do
    logInfo stx.val (e ++ " : " ++ type);
    pure ()

+@[inline] def withDeclId (declId : Syntax) (f : Name → CommandElabM Unit) : CommandElabM Unit := do
+-- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
+let id             := declId.getIdAt 0;
+let optUnivDeclStx := declId.getArg 1;
+savedLevelNames ← getLevelNames;
+levelNames      ←
+  if optUnivDeclStx.isNone then
+    pure savedLevelNames
+  else do {
+    let extraLevels := (optUnivDeclStx.getArg 1).getArgs.getEvenElems;
+    extraLevels.foldlM
+      (fun levelNames idStx =>
+        let id := idStx.getId;
+        if levelNames.elem id then
+          throwAlreadyDeclaredUniverseLevel idStx id
+        else
+          pure (id :: levelNames))
+      savedLevelNames
+  };
+let ref := declId;
+match id with
+| Name.str pre s _ => withNamespace ref pre $ do
+  modifyScope $ fun scope => { levelNames := levelNames, .. scope };
+  finally (f (mkNameSimple s)) (modifyScope $ fun scope => { levelNames := savedLevelNames, .. scope })
+| _                => throwError ref "invalid declaration name"
+
+/--
+  Sort the given list of `usedParams` using the following order:
+  - If it is an explicit level `explicitParams`, then use user given order.
+  - Otherwise, use lexicographical.
+
+  Remark: `explicitParams` are in reverse declaration order. That is, the head is the last declared parameter. -/
+def sortDeclLevelParams (explicitParams : List Name) (usedParams : Array Name) : List Name :=
+let result := explicitParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) [];
+let remaining := usedParams.filter (fun levelParam => !explicitParams.elem levelParam);
+let remaining := remaining.qsort Name.lt;
+result ++ remaining.toList
+
+def addDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := do
+env ← getEnv;
+match env.addDecl decl with
+| Except.ok    env => modify $ fun s => { env := env, .. s }
+| Except.error kex => do
+  opts ← getOptions;
+  throwError ref (kex.toMessageData opts)
+
 end Command
 end Elab
 end Lean
--- a/stage0/src/Init/Lean/Elab/DeclModifiers.lean
+++ b/stage0/src/Init/Lean/Elab/DeclModifiers.lean
@ -0,0 +1,128 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Elab.Command
+
+namespace Lean
+namespace Elab
+namespace Command
+
+structure Attribute :=
+(name : Name) (args : Syntax := Syntax.missing)
+
+instance Attribute.hasFormat : HasFormat Attribute :=
+⟨fun attr => Format.bracket "@[" (toString attr.name ++ (if attr.args.isMissing then "" else toString attr.args)) "]"⟩
+
+inductive Visibility
+| regular | «protected» | «private»
+
+instance Visibility.hasToString : HasToString Visibility :=
+⟨fun v => match v with
+ | Visibility.regular   => "regular"
+ | Visibility.private   => "private"
+ | Visibility.protected => "protected"⟩
+
+structure Modifiers :=
+(docString       : Option String := none)
+(visibility      : Visibility := Visibility.regular)
+(isNoncomputable : Bool := false)
+(isPartial       : Bool := false)
+(isUnsafe        : Bool := false)
+(attrs           : Array Attribute := #[])
+
+def Modifiers.addAttribute (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
+{ attrs := modifiers.attrs.push attr, .. modifiers }
+
+instance Modifiers.hasFormat : HasFormat Modifiers :=
+⟨fun m =>
+  let components : List Format :=
+    (match m.docString with
+     | some str => ["/--" ++ str ++ "-/"]
+     | none     => [])
+    ++ (match m.visibility with
+     | Visibility.regular   => []
+     | Visibility.protected => ["protected"]
+     | Visibility.private   => ["private"])
+    ++ (if m.isNoncomputable then ["noncomputable"] else [])
+    ++ (if m.isPartial then ["partial"] else [])
+    ++ (if m.isUnsafe then ["unsafe"] else [])
+    ++ m.attrs.toList.map (fun attr => fmt attr);
+  Format.bracket "{" (Format.joinSep components ("," ++ Format.line)) "}"⟩
+
+instance Modifiers.hasToString : HasToString Modifiers := ⟨toString ∘ format⟩
+
+def elabAttr (stx : Syntax) : CommandElabM Attribute := do
+-- rawIdent >> many attrArg
+let nameStx := stx.getArg 0;
+attrName ← match nameStx.isIdOrAtom? with
+  | none     => throwError nameStx "identifier expected"
+  | some str => pure $ mkNameSimple str;
+unlessM (liftIO stx (isAttribute attrName)) $
+  throwError stx ("unknown attribute [" ++ attrName ++ "]");
+let args := stx.getArg 1;
+pure { name := attrName, args := args }
+
+def elabAttrs (stx : Syntax) : CommandElabM (Array Attribute) :=
+(stx.getArg 1).foldSepArgsM
+  (fun stx attrs => do
+    attr ← elabAttr stx;
+    pure $ attrs.push attr)
+  #[]
+
+def elabModifiers (stx : Syntax) : CommandElabM Modifiers := do
+let docCommentStx := stx.getArg 0;
+let attrsStx      := stx.getArg 1;
+let visibilityStx := stx.getArg 2;
+let noncompStx    := stx.getArg 3;
+let unsafeStx     := stx.getArg 4;
+let partialStx    := stx.getArg 5;
+docString ← match docCommentStx.getOptional? with
+  | none   => pure none
+  | some s => match s.getArg 1 with
+    | Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
+    | _                 => throwError s ("unexpected doc string " ++ toString (s.getArg 1));
+visibility ← match visibilityStx.getOptional? with
+  | none   => pure Visibility.regular
+  | some v =>
+    let kind := v.getKind;
+    if kind == `Lean.Parser.Command.private then pure Visibility.private
+    else if kind == `Lean.Parser.Command.protected then pure Visibility.protected
+    else throwError v "unexpected visibility modifier";
+attrs ← match attrsStx.getOptional? with
+  | none       => pure #[]
+  | some attrs => elabAttrs attrs;
+pure {
+  docString       := docString,
+  visibility      := visibility,
+  isPartial       := !partialStx.isNone,
+  isUnsafe        := !unsafeStx.isNone,
+  isNoncomputable := !noncompStx.isNone,
+  attrs           := attrs
+}
+
+def mkDeclName (modifiers : Modifiers) (atomicName : Name) : CommandElabM Name := do
+currNamespace ← getCurrNamespace;
+let declName := currNamespace ++ atomicName;
+match modifiers.visibility with
+| Visibility.private => do
+  env ← getEnv;
+  let (env, declName) := mkPrivateName env declName;
+  setEnv env;
+  -- TODO: alias?
+  pure declName
+| _                  => pure declName
+
+def applyAttributes (ref : Syntax) (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit :=
+attrs.forM $ fun attr => do
+ attrImpl ← liftIO ref $ getAttributeImpl attr.name;
+ when (attrImpl.applicationTime == applicationTime) $ do
+   env ← getEnv;
+   env ← liftIO ref $ attrImpl.add env declName attr.args true;
+   setEnv env
+
+end Command
+end Elab
+end Lean
--- a/stage0/src/Init/Lean/Elab/Declaration.lean
+++ b/stage0/src/Init/Lean/Elab/Declaration.lean
@ -4,130 +4,153 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Elab.Command
+import Init.Lean.Util.CollectLevelParams
+import Init.Lean.Elab.Definition

 namespace Lean
 namespace Elab
 namespace Command

-inductive AttributeArg
-| str (val : String)
-| num (val : Nat)
-| id  (val : Name)
+def expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax :=
+-- many Term.bracktedBinder >> Term.optType
+let binders := stx.getArg 0;
+let optType := stx.getArg 1; -- optional (parser! " : " >> termParser)
+if optType.isNone then
+  (binders, none)
+else
+  let typeSpec := optType.getArg 0;
+  (binders, some $ typeSpec.getArg 1)

-instance AttributeArg.hasToString : HasToString AttributeArg :=
-⟨fun arg => match arg with
- | AttributeArg.str v => repr v
- | AttributeArg.num v => toString v
- | AttributeArg.id v  => toString v⟩
+def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
+-- many Term.bracktedBinder >> Term.typeSpec
+let binders := stx.getArg 0;
+let typeSpec := stx.getArg 1;
+(binders, typeSpec.getArg 1)

-structure Attribute :=
-(name : Name) (args : Array AttributeArg)
-
-instance Attribute.hasFormat : HasFormat Attribute :=
-⟨fun attr => Format.bracket "@[" (toString attr.name ++ (Format.prefixJoin " " attr.args.toList)) "]"⟩
-
-inductive Visibility
-| regular | «protected» | «private»
-
-instance Visibility.hasToString : HasToString Visibility :=
-⟨fun v => match v with
- | Visibility.regular   => "regular"
- | Visibility.private   => "private"
- | Visibility.protected => "protected"⟩
-
-structure Modifiers :=
-(docString       : Option String := none)
-(visibility      : Visibility := Visibility.regular)
-(isNoncomputable : Bool := false)
-(isPartial       : Bool := false)
-(isUnsafe        : Bool := false)
-(attrs           : Array Attribute := #[])
-
-instance Modifiers.hasFormat : HasFormat Modifiers :=
-⟨fun m =>
-  let components : List Format :=
-    (match m.docString with
-     | some str => ["/--" ++ str ++ "-/"]
-     | none     => [])
-    ++ (match m.visibility with
-     | Visibility.regular   => []
-     | Visibility.protected => ["protected"]
-     | Visibility.private   => ["private"])
-    ++ (if m.isNoncomputable then ["noncomputable"] else [])
-    ++ (if m.isPartial then ["partial"] else [])
-    ++ (if m.isUnsafe then ["unsafe"] else [])
-    ++ m.attrs.toList.map (fun attr => fmt attr);
-  Format.bracket "{" (Format.joinSep components ("," ++ Format.line)) "}"⟩
-
-instance Modifiers.hasToString : HasToString Modifiers := ⟨toString ∘ format⟩
-
-def elabAttrArg (stx : Syntax) : CommandElabM AttributeArg := do
-match stx.isStrLit? with
-| some v => pure $ AttributeArg.str v
-| _ =>
-match stx.isNatLit? with
-| some v => pure $ AttributeArg.num v
-| _ =>
-match stx with
-| Syntax.ident _ _ v _ => pure $ AttributeArg.id v
-| _ => throwError stx "unexpected attribute argument"
-
-def elabAttr (stx : Syntax) : CommandElabM Attribute := do
-- rawIdent >> many attrArg
-let nameStx := stx.getArg 0;
-attrName ← match nameStx.isIdOrAtom? with
-  | none     => throwError nameStx "identifier expected"
-  | some str => pure $ mkNameSimple str;
-unlessM (liftIO stx (isAttribute attrName)) $
-  throwError stx ("unknown attribute [" ++ attrName ++ "]");
-let argStxs := (stx.getArg 1).getArgs;
-args ← argStxs.mapM elabAttrArg;
-pure { name := attrName, args := args }
-
-def elabAttrs (stx : Syntax) : CommandElabM (Array Attribute) :=
-(stx.getArg 1).foldSepArgsM
-  (fun stx attrs => do
-    attr ← elabAttr stx;
-    pure $ attrs.push attr)
-  #[]
-
-def elabModifiers (stx : Syntax) : CommandElabM Modifiers := do
-let docCommentStx := stx.getArg 0;
-let attrsStx      := stx.getArg 1;
-let visibilityStx := stx.getArg 2;
-let noncompStx    := stx.getArg 3;
-let unsafeStx     := stx.getArg 4;
-let partialStx    := stx.getArg 5;
-docString ← match docCommentStx.getOptional? with
-  | none   => pure none
-  | some s => match s.getArg 1 with
-    | Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
-    | _                 => throwError s ("unexpected doc string " ++ toString (s.getArg 1));
-visibility ← match visibilityStx.getOptional? with
-  | none   => pure Visibility.regular
-  | some v =>
-    let kind := v.getKind;
-    if kind == `Lean.Parser.Command.private then pure Visibility.private
-    else if kind == `Lean.Parser.Command.protected then pure Visibility.protected
-    else throwError v "unexpected visibility modifier";
-attrs ← match attrsStx.getOptional? with
-  | none       => pure #[]
-  | some attrs => elabAttrs attrs;
-pure {
-  docString       := docString,
-  visibility      := visibility,
-  isPartial       := !partialStx.isNone,
-  isUnsafe        := !unsafeStx.isNone,
-  isNoncomputable := !noncompStx.isNone,
-  attrs           := attrs
+def elabAbbrev (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "abbrev " >> declId >> optDeclSig >> declVal
+let (binders, type) := expandOptDeclSig (stx.getArg 2);
+let modifiers       := modifiers.addAttribute { name := `inline };
+let modifiers       := modifiers.addAttribute { name := `reducible };
+elabDefLike {
+  ref := stx, kind := DefKind.def, modifiers := modifiers,
+  declId := stx.getArg 1, binders := binders, type? := type, val := stx.getArg 3
 }

+def elabDef (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "def " >> declId >> optDeclSig >> declVal
+let (binders, type) := expandOptDeclSig (stx.getArg 2);
+elabDefLike {
+  ref := stx, kind := DefKind.def, modifiers := modifiers,
+  declId := stx.getArg 1, binders := binders, type? := type, val := stx.getArg 3
+}
+
+def elabTheorem (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "theorem " >> declId >> declSig >> declVal
+let (binders, type) := expandDeclSig (stx.getArg 2);
+elabDefLike {
+  ref := stx, kind := DefKind.theorem, modifiers := modifiers,
+  declId := stx.getArg 1, binders := binders, type? := some type, val := stx.getArg 3
+}
+
+def elabConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+-- parser! "constant " >> declId >> declSig >> optional declValSimple
+let (binders, type) := expandDeclSig (stx.getArg 2);
+val ← match (stx.getArg 3).getOptional? with
+  | some val => pure val
+  | none     => `(arbitrary _);
+elabDefLike {
+  ref := stx, kind := DefKind.opaque, modifiers := modifiers,
+  declId := stx.getArg 1, binders := binders, type? := some type, val := val
+}
+
+def elabInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+-- parser! "instance " >> optional declId >> declSig >> declVal
+let (binders, type) := expandDeclSig (stx.getArg 2);
+let modifiers       := modifiers.addAttribute { name := `instance };
+declId ← match (stx.getArg 1).getOptional? with
+  | some declId => pure declId
+  | none        => throwError stx "not implemented yet";
+elabDefLike {
+  ref := stx, kind := DefKind.def, modifiers := modifiers,
+  declId := declId, binders := binders, type? := type, val := stx.getArg 3
+}
+
+def elabExample (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "example " >> declSig >> declVal
+let (binders, type) := expandDeclSig (stx.getArg 1);
+let id              := mkIdentFrom stx `_example;
+let declId          := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode];
+elabDefLike {
+  ref := stx, kind := DefKind.example, modifiers := modifiers,
+  declId := declId, binders := binders, type? := some type, val := stx.getArg 2
+}
+
+def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "axiom " >> declId >> declSig
+let declId             := stx.getArg 1;
+let (binders, typeStx) := expandDeclSig (stx.getArg 2);
+withDeclId declId $ fun name => do
+  declName          ← mkDeclName modifiers name;
+  applyAttributes stx declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
+  explictLevelNames ← getLevelNames;
+  decl ← runTermElabM $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
+    type ← Term.elabType typeStx;
+    Term.synthesizeSyntheticMVars false;
+    type ← Term.instantiateMVars typeStx type;
+    type ← Term.mkForall typeStx xs type;
+    (type, _) ← Term.mkForallUsedOnly typeStx vars type;
+    type ← Term.levelMVarToParam type;
+    let usedParams  := collectLevelParams type;
+    let levelParams := sortDeclLevelParams explictLevelNames usedParams;
+    pure $ Declaration.axiomDecl {
+      name     := declName,
+      lparams  := levelParams,
+      type     := type,
+      isUnsafe := modifiers.isUnsafe
+    }
+  };
+  addDecl stx decl;
+  applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
+  applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterCompilation
+
+def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+pure () -- TODO
+
+def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+pure () -- TODO
+
+def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+pure () -- TODO
+
@[builtinCommandElab declaration]
 def elabDeclaration : CommandElab :=
 fun stx => do
  modifiers ← elabModifiers (stx.getArg 0);
-  throwError stx.val ("wip, modifiers: " ++ toString modifiers)
+  let decl     := stx.getArg 1;
+  let declKind := decl.getKind;
+  if declKind == `Lean.Parser.Command.abbrev then
+    elabAbbrev modifiers decl
+  else if declKind == `Lean.Parser.Command.def then
+    elabDef modifiers decl
+  else if declKind == `Lean.Parser.Command.theorem then
+    elabTheorem modifiers decl
+  else if declKind == `Lean.Parser.Command.constant then
+    elabConstant modifiers decl
+  else if declKind == `Lean.Parser.Command.instance then
+    elabInstance modifiers decl
+  else if declKind == `Lean.Parser.Command.axiom then
+    elabAxiom modifiers decl
+  else if declKind == `Lean.Parser.Command.example then
+    elabExample modifiers decl
+  else if declKind == `Lean.Parser.Command.inductive then
+    elabInductive modifiers decl
+  else if declKind == `Lean.Parser.Command.classInductive then
+    elabClassInductive modifiers decl
+  else if declKind == `Lean.Parser.Command.structure then
+    elabStructure modifiers decl
+  else
+    throwError stx.val "unexpected declaration"

 end Command
 end Elab
--- a/stage0/src/Init/Lean/Elab/Definition.lean
+++ b/stage0/src/Init/Lean/Elab/Definition.lean
@ -0,0 +1,47 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Elab.DeclModifiers
+
+namespace Lean
+namespace Elab
+
+namespace Command
+
+inductive DefKind
+| «def» | «theorem» | «example» | «opaque»
+
+structure DefView :=
+(kind          : DefKind)
+(ref           : Syntax)
+(modifiers     : Modifiers)
+(declId        : Syntax)
+(binders       : Syntax)
+(type?         : Option Syntax)
+(val           : Syntax)
+
+def elabDefLike (view : DefView) : CommandElabM Unit :=
+withDeclId view.declId $ fun name => do
+  currNamespace ← getCurrNamespace;
+  runTermElabM $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>
+    match view.type? with
+    | some typeStx => do
+      type    ← Term.elabType typeStx;
+      Term.synthesizeSyntheticMVars false;
+      type    ← Term.instantiateMVars typeStx type;
+      defType ← Term.mkForall typeStx xs type;
+      -- TODO: unassigned universe metavariables to new parameters
+      -- TODO: if theorem, filter unused vars
+      Term.dbgTrace (">>> " ++ toString type);
+      pure ()
+    | none => do
+      type ← Term.mkFreshTypeMVar view.binders;
+
+      pure ()
+
+end Command
+end Elab
+end Lean
--- a/stage0/src/Init/Lean/Elab/Frontend.lean
+++ b/stage0/src/Init/Lean/Elab/Frontend.lean
@ -79,7 +79,7 @@ open Frontend
 def IO.processCommands (parserCtx : Parser.ParserContextCore) (parserStateRef : IO.Ref Parser.ModuleParserState) (cmdStateRef : IO.Ref Command.State) : IO Unit := do
 ps ← parserStateRef.get;
 cmdPosRef ← IO.mkRef ps.pos;
-EIO.adaptExcept (fun (ex : Empty) => unreachable!) $ -- TODO: compiler support for Empty.rec is missing
+EIO.adaptExcept (fun (ex : Empty) => Empty.rec _ ex) $
  processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, parserCtx := parserCtx }

 def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
--- a/stage0/src/Init/Lean/Elab/Level.lean
+++ b/stage0/src/Init/Lean/Elab/Level.lean
@ -16,7 +16,7 @@ structure Context :=
 (fileName   : String)
 (fileMap    : FileMap)
 (cmdPos     : String.Pos)
-(univNames  : List Name := [])
+(levelNames : List Name)

 structure State :=
 (ngen : NameGenerator)
@ -70,7 +70,7 @@ partial def elabLevel : Syntax → LevelElabM Level
  else if kind == `Lean.Parser.Level.ident then do
    let paramName := stx.getIdAt 0;
    ctx ← read;
-    unless (ctx.univNames.contains paramName) $ throwError stx ("unknown universe level " ++ paramName);
+    unless (ctx.levelNames.contains paramName) $ throwError stx ("unknown universe level " ++ paramName);
    pure $ mkLevelParam paramName
  else if kind == `Lean.Parser.Level.addLit then do
    lvl ← elabLevel (stx.getArg 0);
--- a/stage0/src/Init/Lean/Elab/Term.lean
+++ b/stage0/src/Init/Lean/Elab/Term.lean
@ -22,7 +22,7 @@ structure Context extends Meta.Context :=
 (fileMap         : FileMap)
 (cmdPos          : String.Pos)
 (currNamespace   : Name)
-(univNames       : List Name       := [])
+(levelNames      : List Name       := [])
 (openDecls       : List OpenDecl   := [])
 (macroStack      : List Syntax     := [])
 (currMacroScope  : MacroScope      := 0)
@ -146,7 +146,7 @@ match expectedMsg with
 | none    => throwError ref ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
 | some ex => throwError ref ("unexpected syntax, expected '" ++ ex ++ "'" ++ MessageData.nest 2 (Format.line ++ refFmt))

-protected def getCurrMacroScope : TermElabM Nat := do
+protected def getCurrMacroScope : TermElabM MacroScope := do
 ctx ← read;
 pure ctx.currMacroScope

@ -285,6 +285,7 @@ def mkFreshTypeMVar (ref : Syntax) (kind : MetavarKind := MetavarKind.natural) (
 liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
 def getLevel (ref : Syntax) (type : Expr) : TermElabM Level := liftMetaM ref $ Meta.getLevel type
 def mkForall (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkForall xs e
+def mkForallUsedOnly (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM (Expr × Nat) := liftMetaM ref $ Meta.mkForallUsedOnly xs e
 def mkLambda (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkLambda xs e
 def mkLet (ref : Syntax) (x : Expr) (e : Expr) : TermElabM Expr := mkLambda ref #[x] e
 def trySynthInstance (ref : Syntax) (type : Expr) : TermElabM (LOption Expr) := liftMetaM ref $ Meta.trySynthInstance type
@ -329,6 +330,14 @@ stx.ifNode x (fun _ => throwError stx ("term elaborator failed, unexpected synta
 def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
 mkNode `Lean.Parser.Term.explicitBinder #[mkAtom "(", mkNullNode #[ident], mkNullNode #[mkAtom ":", type], mkNullNode, mkAtom ")"]

+/-- Convert unassigned universe level metavariables into parameters. -/
+def levelMVarToParam (e : Expr) : TermElabM Expr := do
+ctx ← read;
+mctx ← getMCtx;
+let r := mctx.levelMVarToParam (fun n => ctx.levelNames.elem n) e;
+modify $ fun s => { mctx := r.mctx, .. s };
+pure r.expr
+
 /--
  Auxiliary method for creating fresh binder names.
  Do not confuse with the method for creating fresh free/meta variable ids. -/
--- a/stage0/src/Init/Lean/Elab/Util.lean
+++ b/stage0/src/Init/Lean/Elab/Util.lean
@ -60,7 +60,7 @@ table ← builtinTableRef.get;
 pure { table := table }

 private def throwUnexpectedElabType {γ} (typeName : Name) (constName : Name) : ExceptT String Id γ :=
-throw ("unexpected elaborator type at '" ++ toString constName ++ "' `" ++ toString typeName ++ "` expected")
+throw ("unexpected elaborator type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected")

 private unsafe def mkElabFnOfConstantUnsafe (γ) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ :=
 match env.find? constName with
--- a/stage0/src/Init/Lean/Expr.lean
+++ b/stage0/src/Init/Lean/Expr.lean
@ -554,7 +554,9 @@ constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool := arbitrary _
 /--
  Lower the loose bound variables `>= s` in `e` by `d`.
  That is, a loose bound variable `bvar i`.
-  `i >= s` is mapped into `bvar (i-d)`. -/
+  `i >= s` is mapped into `bvar (i-d)`.
+
+  Remark: if `s < d`, then result is `e` -/
@[extern "lean_expr_lower_loose_bvars"]
 constant lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _

--- a/stage0/src/Init/Lean/Level.lean
+++ b/stage0/src/Init/Lean/Level.lean
@ -7,6 +7,8 @@ prelude
 import Init.Data.Option.Basic
 import Init.Data.HashMap
 import Init.Data.PersistentHashMap
+import Init.Data.HashSet
+import Init.Data.PersistentHashSet
 import Init.Lean.Data.Name
 import Init.Lean.Data.Format

@ -432,6 +434,9 @@ end Level

 abbrev LevelMap (α : Type)  := HashMap Level α
 abbrev PersistentLevelMap (α : Type) := PHashMap Level α
+abbrev LevelSet := HashSet Level
+abbrev PersistentLevelSet := PHashSet Level
+abbrev PLevelSet := PersistentLevelSet

 end Lean

--- a/stage0/src/Init/Lean/Meta/Basic.lean
+++ b/stage0/src/Init/Lean/Meta/Basic.lean
@ -390,6 +390,9 @@ if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkForall xs e
 def mkLambda (xs : Array Expr) (e : Expr) : MetaM Expr :=
 if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkLambda xs e

+def mkForallUsedOnly (xs : Array Expr) (e : Expr) : MetaM (Expr × Nat) :=
+if xs.isEmpty then pure (e, 0) else liftMkBindingM $ MetavarContext.mkForallUsedOnly xs e
+
 /-- Save cache, execute `x`, restore cache -/
@[inline] def savingCache {α} (x : MetaM α) : MetaM α := do
 s ← get;
--- a/stage0/src/Init/Lean/Meta/Instances.lean
+++ b/stage0/src/Init/Lean/Meta/Instances.lean
@ -48,7 +48,7 @@ registerAttribute {
  name  := `instance,
  descr := "type class instance",
  add   := fun env declName args persistent => do
-    unless args.isMissing $ throw (IO.userError ("invalid attribute 'instance', unexpected argument"));
+    when args.hasArgs $ throw (IO.userError ("invalid attribute 'instance', unexpected argument"));
    unless persistent $ throw (IO.userError ("invalid attribute 'instance', must be persistent"));
    env ← IO.ofExcept (addGlobalInstanceOld env declName); -- TODO: delete
    addGlobalInstance env declName
--- a/stage0/src/Init/Lean/MetavarContext.lean
+++ b/stage0/src/Init/Lean/MetavarContext.lean
@ -813,49 +813,61 @@ if !e.hasMVar then
 else
  withFreshCache $ elimMVarDepsAux xs e

-/-- Similar to `Expr.abstractRange`, but handles metavariables correctly.
-    It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
-    contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.
+/--
+  Similar to `Expr.abstractRange`, but handles metavariables correctly.
+  It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
+  contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.

-    `elimMVarDeps` is defined later in this file. -/
+  `elimMVarDeps` is defined later in this file. -/
@[inline] private def abstractRange (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do
 e ← elimMVarDeps xs e;
 pure (e.abstractRange i xs)

-/-- Similar to `LocalContext.mkBinding`, but handles metavariables correctly. -/
-@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) : M Expr := do
+/--
+  Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
+  If `usedOnly == false` then `forall` and `lambda` are created only for used variables. -/
+@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) : M (Expr × Nat) := do
 e ← abstractRange xs xs.size e;
 xs.size.foldRevM
-  (fun i e =>
+  (fun i (p : Expr × Nat) =>
+    let (e, num) := p;
    let x := xs.get! i;
    match lctx.getFVar! x with
-    | LocalDecl.cdecl _ _ n type bi => do
-      type ← abstractRange xs i type;
-      if isLambda then
-        pure $ Lean.mkLambda n bi type e
+    | LocalDecl.cdecl _ _ n type bi =>
+      if !usedOnly || e.hasLooseBVar 0 then do
+        type ← abstractRange xs i type;
+        if isLambda then
+          pure (Lean.mkLambda n bi type e, num + 1)
+        else
+          pure (Lean.mkForall n bi type e, num + 1)
      else
-        pure $ Lean.mkForall n bi type e
+        pure (e.lowerLooseBVars 1 1, num)
    | LocalDecl.ldecl _ _ n type value => do
      if e.hasLooseBVar 0 then do
        type  ← abstractRange xs i type;
        value ← abstractRange xs i value;
-        pure $ mkLet n type value e
+        pure (mkLet n type value e, num + 1)
      else
-        pure e)
-  e
+        pure (e.lowerLooseBVars 1 1, num))
+  (e, 0)

 end MkBinding

 abbrev MkBindingM := ReaderT LocalContext MkBinding.M

-def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) : MkBindingM Expr :=
-fun lctx => MkBinding.mkBinding isLambda lctx xs e
+def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) : MkBindingM (Expr × Nat) :=
+fun lctx => MkBinding.mkBinding isLambda lctx xs e usedOnly

-@[inline] def mkLambda (xs : Array Expr) (e : Expr) : MkBindingM Expr :=
-mkBinding true xs e
+@[inline] def mkLambda (xs : Array Expr) (e : Expr) : MkBindingM Expr := do
+(e, _) ← mkBinding true xs e;
+pure e

-@[inline] def mkForall (xs : Array Expr) (e : Expr) : MkBindingM Expr :=
-mkBinding false xs e
+@[inline] def mkForall (xs : Array Expr) (e : Expr) : MkBindingM Expr := do
+(e, _) ← mkBinding false xs e;
+pure e
+
+@[inline] def mkForallUsedOnly (xs : Array Expr) (e : Expr) : MkBindingM (Expr × Nat) := do
+mkBinding false xs e true

 /--
  `isWellFormed mctx lctx e` return true if
@ -881,5 +893,77 @@ partial def isWellFormed (mctx : MetavarContext) (lctx : LocalContext) : Expr
 | Expr.fvar fvarId _       => lctx.contains fvarId
 | Expr.localE _ _ _ _      => unreachable!

+
+namespace LevelMVarToParam
+
+structure Context :=
+(paramNamePrefix : Name)
+(alreadyUsedPred : Name → Bool)
+
+structure State :=
+(mctx         : MetavarContext)
+(paramNames   : Array Name := #[])
+(nextParamIdx : Nat)
+
+abbrev M := ReaderT Context $ StateM State
+
+partial def mkParamName : Unit → M Name
+| _ => do
+  ctx ← read;
+  s ← get;
+  let newParamName := ctx.paramNamePrefix.appendIndexAfter s.nextParamIdx;
+  if ctx.alreadyUsedPred newParamName then do
+    modify $ fun s => { nextParamIdx := s.nextParamIdx + 1, .. s};
+    mkParamName ()
+  else do
+    modify $ fun s => { nextParamIdx := s.nextParamIdx + 1, paramNames := s.paramNames.push newParamName, .. s};
+    pure newParamName
+
+partial def visitLevel : Level → M Level
+| u@(Level.succ v _)      => do v ← visitLevel v; pure (u.updateSucc v rfl)
+| u@(Level.max v₁ v₂ _)   => do v₁ ← visitLevel v₁; v₂ ← visitLevel v₂; pure (u.updateMax v₁ v₂ rfl)
+| u@(Level.imax v₁ v₂ _)  => do v₁ ← visitLevel v₁; v₂ ← visitLevel v₂; pure (u.updateIMax v₁ v₂ rfl)
+| u@(Level.zero _)        => pure u
+| u@(Level.param _ _)     => pure u
+| u@(Level.mvar mvarId _) => do
+  s ← get;
+  match s.mctx.getLevelAssignment? mvarId with
+  | some v => visitLevel v
+  | none   => do
+    p ← mkParamName ();
+    let p := mkLevelParam p;
+    modify $ fun s => { mctx := s.mctx.assignLevel mvarId p, .. s };
+    pure p
+
+@[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=
+if e.hasLevelMVar then f e else pure e
+
+partial def main : Expr → M Expr
+| e@(Expr.proj _ _ s _)    => do s ← visit main s; pure (e.updateProj! s)
+| e@(Expr.forallE _ d b _) => do d ← visit main d; b ← visit main b; pure (e.updateForallE! d b)
+| e@(Expr.lam _ d b _)     => do d ← visit main d; b ← visit main b; pure (e.updateLambdaE! d b)
+| e@(Expr.letE _ t v b _)  => do t ← visit main t; v ← visit main v; b ← visit main b; pure (e.updateLet! t v b)
+| e@(Expr.app f a _)       => do f ← visit main f; a ← visit main a; pure (e.updateApp! f a)
+| e@(Expr.mdata _ b _)     => do b ← visit main b; pure (e.updateMData! b)
+| e@(Expr.const _ us _)    => do us ← us.mapM visitLevel; pure (e.updateConst! us)
+| e@(Expr.sort u _)        => do u ← visitLevel u; pure (e.updateSort! u)
+| e                        => pure e
+
+end LevelMVarToParam
+
+structure UnivMVarParamResult :=
+(mctx          : MetavarContext)
+(newParamNames : Array Name)
+(nextParamIdx  : Nat)
+(expr          : Expr)
+
+def levelMVarToParam (mctx : MetavarContext) (alreadyUsedPred : Name → Bool) (e : Expr) (paramNamePrefix : Name := `u) (nextParamIdx : Nat := 1)
+    : UnivMVarParamResult :=
+let (e, s) := LevelMVarToParam.main e { paramNamePrefix := paramNamePrefix, alreadyUsedPred := alreadyUsedPred } { mctx := mctx, nextParamIdx := nextParamIdx };
+{ mctx          := mctx,
+  newParamNames := s.paramNames,
+  nextParamIdx  := s.nextParamIdx,
+  expr          := e }
+
 end MetavarContext
 end Lean
--- a/stage0/src/Init/Lean/Parser/Parser.lean
+++ b/stage0/src/Init/Lean/Parser/Parser.lean
@ -1515,7 +1515,7 @@ registerAttribute {
 name  := attrName,
 descr := "Builtin parser",
 add   := fun env declName args persistent => do {
-   unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
+   when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
   unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent"));
   match env.find? declName with
   | none  => throw "unknown declaration"
--- a/stage0/src/Init/Lean/Util/CollectLevelParams.lean
+++ b/stage0/src/Init/Lean/Util/CollectLevelParams.lean
@ -0,0 +1,61 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Expr
+
+namespace Lean
+
+namespace CollectLevelParams
+
+structure State :=
+(visitedLevel : LevelSet   := {})
+(visitedExpr  : ExprSet    := {})
+(params       : Array Name := #[])
+
+abbrev M := StateM State
+
+@[inline] def visitLevel (f : Level → M Unit) (u : Level) : M Unit :=
+if !u.hasParam then pure ()
+else do
+  s ← get;
+  if s.visitedLevel.contains u then pure ()
+  else do
+    modify $ fun s => { visitedLevel := s.visitedLevel.insert u, .. s };
+    f u
+
+partial def collect : Level → M Unit
+| Level.succ v _    => visitLevel collect v
+| Level.max u v _   => do visitLevel collect u; visitLevel collect v
+| Level.imax u v _  => do visitLevel collect u; visitLevel collect v
+| Level.param n _   => modify $ fun s => { params := s.params.push n, .. s }
+| _                 => pure ()
+
+@[inline] def visitExpr (f : Expr → M Unit) (e : Expr) : M Unit :=
+if !e.hasLevelParam then pure ()
+else do
+  s ← get;
+  if s.visitedExpr.contains e then pure ()
+  else do
+    modify $ fun s => { visitedExpr := s.visitedExpr.insert e, .. s };
+    f e
+
+partial def main : Expr → M Unit
+| Expr.proj _ _ s _    => visitExpr main s
+| Expr.forallE _ d b _ => do visitExpr main d; visitExpr main b
+| Expr.lam _ d b _     => do visitExpr main d; visitExpr main b
+| Expr.letE _ t v b _  => do visitExpr main t; visitExpr main v; visitExpr main b
+| Expr.app f a _       => do visitExpr main f; visitExpr main a
+| Expr.mdata _ b _     => visitExpr main b
+| Expr.const _ us _    => us.forM (visitLevel collect)
+| Expr.sort u _        => visitLevel collect u
+| _                    => pure ()
+
+end CollectLevelParams
+
+def collectLevelParams (e : Expr) : Array Name :=
+(CollectLevelParams.main e {}).2.params
+
+end Lean
--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
--- a/stage0/stdlib/Init/Data/Array/Basic.c
+++ b/stage0/stdlib/Init/Data/Array/Basic.c
@ -25,6 +25,7 @@ lean_object* l_Array_iterateM_u2082Aux___main(lean_object*, lean_object*);
 lean_object* l_Array_iterate_u2082(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_extractAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_HasBeq(lean_object*);
+lean_object* l_Array_elem___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Array_anyFrom___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_indexOfAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Array_allRangeM___spec__1___boxed(lean_object*, lean_object*);
@ -414,6 +415,7 @@ lean_object* l_List_redLength(lean_object*);
 lean_object* l_Array_findMAux___boxed(lean_object*, lean_object*);
 lean_object* l_Array_findRev_x21___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_insertAtAux___rarg___boxed(lean_object*, lean_object*, lean_object*);
+uint8_t l_Array_elem___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_find_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlM___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_Basic_1__swapAtPanic_x21___at_Array_swapAt_x21___spec__1___rarg(lean_object*, lean_object*);
@ -525,6 +527,7 @@ lean_object* l___private_Init_Data_Array_Basic_4__foldrRangeMAux___rarg___boxed(
 lean_object* l_Array_isEqvAux___main(lean_object*);
 lean_object* l_Array_insertAt(lean_object*);
 lean_object* l_Array_foldlFromM(lean_object*, lean_object*);
+lean_object* l_Array_elem(lean_object*);
 lean_object* l_Array_filter___rarg(lean_object*, lean_object*);
 lean_object* l_Array_forRevMAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_HasRepr(lean_object*);
@ -7243,6 +7246,32 @@ x_5 = lean_box(x_4);
 return x_5;
 }
 }
+uint8_t l_Array_elem___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint8_t x_4; 
+x_4 = l_Array_contains___rarg(x_1, x_3, x_2);
+return x_4;
+}
+}
+lean_object* l_Array_elem(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Array_elem___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Array_elem___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint8_t x_4; lean_object* x_5; 
+x_4 = l_Array_elem___rarg(x_1, x_2, x_3);
+lean_dec(x_3);
+x_5 = lean_box(x_4);
+return x_5;
+}
+}
 lean_object* l_Array_insertAtAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -7321,7 +7350,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Data_Array_Basic_1__swapAtPanic_x21___rarg___closed__3;
-x_2 = lean_unsigned_to_nat(602u);
+x_2 = lean_unsigned_to_nat(605u);
 x_3 = lean_unsigned_to_nat(20u);
 x_4 = l_Array_insertAt___rarg___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
--- a/stage0/stdlib/Init/Lean/Attributes.c
+++ b/stage0/stdlib/Init/Lean/Attributes.c
@ -93,11 +93,14 @@ lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_
 uint8_t l_AssocList_contains___main___at_Lean_registerAttribute___spec__2(lean_object*, lean_object*);
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
 lean_object* l_Lean_registerTagAttribute___lambda__4___closed__3;
+lean_object* l_Lean_Syntax_hasArgs___boxed(lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_registerParametricAttribute___spec__5(lean_object*);
 lean_object* l_HashMapImp_find_x3f___at_Lean_getAttributeImpl___spec__1(lean_object*, lean_object*);
+uint8_t l_Lean_AttributeApplicationTime_beq(uint8_t, uint8_t);
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_TagAttribute_Inhabited___closed__2;
 lean_object* l_Lean_registerEnumAttributes___rarg___lambda__2___closed__2;
+lean_object* l_Lean_AttributeApplicationTime_hasBeq;
 lean_object* lean_array_fget(lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_TagAttribute_Inhabited___closed__1;
@ -112,6 +115,7 @@ lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_registerParametricAttribute___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__2;
 lean_object* l_Lean_AttributeImpl_inhabited___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_AttributeApplicationTime_hasBeq___closed__1;
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_registerEnumAttributes___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkAttributeMapRef(lean_object*);
@ -179,7 +183,6 @@ lean_object* l_Array_binSearchAux___main___at_Lean_EnumAttributes_getValue___spe
 lean_object* l_Lean_AttributeImpl_inhabited___closed__6;
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_AssocList_replace___main___at_Lean_registerAttribute___spec__7(lean_object*, lean_object*, lean_object*);
-uint8_t l_Lean_Syntax_isMissing(lean_object*);
 lean_object* l_Array_qsortAux___main___at_Lean_registerEnumAttributes___spec__2(lean_object*);
 lean_object* l_Array_qsortAux___main___at_Lean_registerEnumAttributes___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_AssocList_find___main___at_Lean_getAttributeImpl___spec__2___boxed(lean_object*, lean_object*);
@ -194,6 +197,7 @@ lean_object* l_Lean_AttributeImpl_inhabited___lambda__2___boxed(lean_object*, le
 extern lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__4___closed__2;
 lean_object* l_Lean_AttributeImpl_inhabited___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_registerParametricAttribute___spec__8(lean_object*);
+uint8_t l_Lean_Syntax_hasArgs(lean_object*);
 lean_object* l_Lean_registerTagAttribute___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
@ -209,6 +213,7 @@ lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_
 lean_object* l_Lean_registerEnumAttributes___rarg___closed__1;
 lean_object* l_RBNode_fold___main___at_Lean_registerParametricAttribute___spec__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_AttributeImpl_inhabited___closed__1;
+lean_object* l_Lean_AttributeApplicationTime_beq___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_ParametricAttribute_getParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__4;
 lean_object* lean_add_attribute(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
@ -309,6 +314,127 @@ lean_object* l_Lean_EnumAttributes_getValue(lean_object*);
 lean_object* l_Lean_registerEnumAttributes___rarg(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_registerParametricAttribute___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+uint8_t l_Lean_AttributeApplicationTime_beq(uint8_t x_1, uint8_t x_2) {
+_start:
+{
+switch (x_1) {
+case 0:
+{
+lean_object* x_3; 
+x_3 = lean_box(x_2);
+if (lean_obj_tag(x_3) == 0)
+{
+uint8_t x_4; 
+x_4 = 1;
+return x_4;
+}
+else
+{
+uint8_t x_5; 
+lean_dec(x_3);
+x_5 = 0;
+return x_5;
+}
+}
+case 1:
+{
+lean_object* x_6; 
+x_6 = lean_box(x_2);
+if (lean_obj_tag(x_6) == 1)
+{
+uint8_t x_7; 
+x_7 = 1;
+return x_7;
+}
+else
+{
+uint8_t x_8; 
+lean_dec(x_6);
+x_8 = 0;
+return x_8;
+}
+}
+default: 
+{
+lean_object* x_9; 
+x_9 = lean_box(x_2);
+if (lean_obj_tag(x_9) == 2)
+{
+uint8_t x_10; 
+x_10 = 1;
+return x_10;
+}
+else
+{
+uint8_t x_11; 
+lean_dec(x_9);
+x_11 = 0;
+return x_11;
+}
+}
+}
+}
+}
+lean_object* l_Lean_AttributeApplicationTime_beq___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6; 
+x_3 = lean_unbox(x_1);
+lean_dec(x_1);
+x_4 = lean_unbox(x_2);
+lean_dec(x_2);
+x_5 = l_Lean_AttributeApplicationTime_beq(x_3, x_4);
+x_6 = lean_box(x_5);
+return x_6;
+}
+}
+lean_object* _init_l_Lean_AttributeApplicationTime_hasBeq___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_AttributeApplicationTime_beq___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Lean_AttributeApplicationTime_hasBeq() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_AttributeApplicationTime_hasBeq___closed__1;
+return x_1;
+}
+}
+uint8_t l_Lean_Syntax_hasArgs(lean_object* x_1) {
+_start:
+{
+if (lean_obj_tag(x_1) == 1)
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_2 = lean_ctor_get(x_1, 1);
+x_3 = lean_array_get_size(x_2);
+x_4 = lean_unsigned_to_nat(0u);
+x_5 = lean_nat_dec_lt(x_4, x_3);
+lean_dec(x_3);
+return x_5;
+}
+else
+{
+uint8_t x_6; 
+x_6 = 0;
+return x_6;
+}
+}
+}
+lean_object* l_Lean_Syntax_hasArgs___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_Syntax_hasArgs(x_1);
+lean_dec(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
 lean_object* l_Lean_AttributeImpl_inhabited___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) {
 _start:
 {
@ -3483,7 +3609,7 @@ lean_object* _init_l_Lean_registerTagAttribute___lambda__4___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("', unexpected argument");
+x_1 = lean_mk_string("', must be persistent");
 return x_1;
 }
 }
@ -3491,7 +3617,7 @@ lean_object* _init_l_Lean_registerTagAttribute___lambda__4___closed__3() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("', must be persistent");
+x_1 = lean_mk_string("', ");
 return x_1;
 }
 }
@ -3499,7 +3625,7 @@ lean_object* _init_l_Lean_registerTagAttribute___lambda__4___closed__4() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("', ");
+x_1 = lean_mk_string("', declaration is in an imported module");
 return x_1;
 }
 }
@ -3507,7 +3633,7 @@ lean_object* _init_l_Lean_registerTagAttribute___lambda__4___closed__5() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("', declaration is in an imported module");
+x_1 = lean_mk_string("', unexpected argument");
 return x_1;
 }
 }
@ -3515,9 +3641,11 @@ lean_object* l_Lean_registerTagAttribute___lambda__4(lean_object* x_1, lean_obje
 _start:
 {
 uint8_t x_9; 
-x_9 = l_Lean_Syntax_isMissing(x_6);
+x_9 = l_Lean_Syntax_hasArgs(x_6);
 if (x_9 == 0)
 {
+if (x_7 == 0)
+{
 lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
 lean_dec(x_5);
 lean_dec(x_4);
@ -3537,74 +3665,74 @@ return x_16;
 }
 else
 {
-if (x_7 == 0)
+lean_object* x_17; 
+x_17 = l_Lean_Environment_getModuleIdxFor_x3f(x_4, x_5);
+if (lean_obj_tag(x_17) == 0)
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+lean_object* x_18; 
+lean_inc(x_5);
+lean_inc(x_4);
+x_18 = lean_apply_2(x_2, x_4, x_5);
+if (lean_obj_tag(x_18) == 0)
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_19 = lean_ctor_get(x_18, 0);
+lean_inc(x_19);
+lean_dec(x_18);
+x_20 = l_Lean_Name_toString___closed__1;
+x_21 = l_Lean_Name_toStringWithSep___main(x_20, x_1);
+x_22 = l_Lean_registerTagAttribute___lambda__4___closed__1;
+x_23 = lean_string_append(x_22, x_21);
+lean_dec(x_21);
+x_24 = l_Lean_registerTagAttribute___lambda__4___closed__3;
+x_25 = lean_string_append(x_23, x_24);
+x_26 = lean_string_append(x_25, x_19);
+lean_dec(x_19);
+x_27 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_27, 0, x_26);
+lean_ctor_set(x_27, 1, x_8);
+return x_27;
+}
+else
+{
+lean_object* x_28; lean_object* x_29; 
+lean_dec(x_18);
+lean_dec(x_1);
+x_28 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_3, x_4, x_5);
+x_29 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_29, 0, x_28);
+lean_ctor_set(x_29, 1, x_8);
+return x_29;
+}
+}
+else
+{
+lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+lean_dec(x_17);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-x_17 = l_Lean_Name_toString___closed__1;
-x_18 = l_Lean_Name_toStringWithSep___main(x_17, x_1);
-x_19 = l_Lean_registerTagAttribute___lambda__4___closed__1;
-x_20 = lean_string_append(x_19, x_18);
-lean_dec(x_18);
-x_21 = l_Lean_registerTagAttribute___lambda__4___closed__3;
-x_22 = lean_string_append(x_20, x_21);
-x_23 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_23, 0, x_22);
-lean_ctor_set(x_23, 1, x_8);
-return x_23;
-}
-else
-{
-lean_object* x_24; 
-x_24 = l_Lean_Environment_getModuleIdxFor_x3f(x_4, x_5);
-if (lean_obj_tag(x_24) == 0)
-{
-lean_object* x_25; 
-lean_inc(x_5);
-lean_inc(x_4);
-x_25 = lean_apply_2(x_2, x_4, x_5);
-if (lean_obj_tag(x_25) == 0)
-{
-lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; 
-lean_dec(x_5);
-lean_dec(x_4);
-lean_dec(x_3);
-x_26 = lean_ctor_get(x_25, 0);
-lean_inc(x_26);
-lean_dec(x_25);
-x_27 = l_Lean_Name_toString___closed__1;
-x_28 = l_Lean_Name_toStringWithSep___main(x_27, x_1);
-x_29 = l_Lean_registerTagAttribute___lambda__4___closed__1;
-x_30 = lean_string_append(x_29, x_28);
-lean_dec(x_28);
-x_31 = l_Lean_registerTagAttribute___lambda__4___closed__4;
-x_32 = lean_string_append(x_30, x_31);
-x_33 = lean_string_append(x_32, x_26);
-lean_dec(x_26);
-x_34 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_34, 0, x_33);
-lean_ctor_set(x_34, 1, x_8);
-return x_34;
-}
-else
-{
-lean_object* x_35; lean_object* x_36; 
-lean_dec(x_25);
-lean_dec(x_1);
-x_35 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_3, x_4, x_5);
-x_36 = lean_alloc_ctor(0, 2, 0);
+x_30 = l_Lean_Name_toString___closed__1;
+x_31 = l_Lean_Name_toStringWithSep___main(x_30, x_1);
+x_32 = l_Lean_registerTagAttribute___lambda__4___closed__1;
+x_33 = lean_string_append(x_32, x_31);
+lean_dec(x_31);
+x_34 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_35 = lean_string_append(x_33, x_34);
+x_36 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_36, 0, x_35);
 lean_ctor_set(x_36, 1, x_8);
 return x_36;
 }
 }
+}
 else
 {
 lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
-lean_dec(x_24);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
@ -3623,8 +3751,6 @@ return x_43;
 }
 }
 }
-}
-}
 lean_object* l_Lean_registerTagAttribute___lambda__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
@ -5353,7 +5479,7 @@ x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_1);
 x_12 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_13 = lean_string_append(x_12, x_11);
 lean_dec(x_11);
-x_14 = l_Lean_registerTagAttribute___lambda__4___closed__3;
+x_14 = l_Lean_registerTagAttribute___lambda__4___closed__2;
 x_15 = lean_string_append(x_13, x_14);
 x_16 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_16, 0, x_15);
@ -5385,7 +5511,7 @@ x_21 = l_Lean_Name_toStringWithSep___main(x_20, x_1);
 x_22 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_23 = lean_string_append(x_22, x_21);
 lean_dec(x_21);
-x_24 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_24 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_25 = lean_string_append(x_23, x_24);
 x_26 = lean_string_append(x_25, x_19);
 lean_dec(x_19);
@ -5418,7 +5544,7 @@ x_34 = l_Lean_Name_toStringWithSep___main(x_33, x_1);
 x_35 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_36 = lean_string_append(x_35, x_34);
 lean_dec(x_34);
-x_37 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_37 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_38 = lean_string_append(x_36, x_37);
 x_39 = lean_string_append(x_38, x_32);
 lean_dec(x_32);
@ -5456,7 +5582,7 @@ x_44 = l_Lean_Name_toStringWithSep___main(x_43, x_1);
 x_45 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_46 = lean_string_append(x_45, x_44);
 lean_dec(x_44);
-x_47 = l_Lean_registerTagAttribute___lambda__4___closed__5;
+x_47 = l_Lean_registerTagAttribute___lambda__4___closed__4;
 x_48 = lean_string_append(x_46, x_47);
 x_49 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_49, 0, x_48);
@ -7440,7 +7566,7 @@ x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_1);
 x_12 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_13 = lean_string_append(x_12, x_11);
 lean_dec(x_11);
-x_14 = l_Lean_registerTagAttribute___lambda__4___closed__3;
+x_14 = l_Lean_registerTagAttribute___lambda__4___closed__2;
 x_15 = lean_string_append(x_13, x_14);
 x_16 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_16, 0, x_15);
@ -7473,7 +7599,7 @@ x_21 = l_Lean_Name_toStringWithSep___main(x_20, x_1);
 x_22 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_23 = lean_string_append(x_22, x_21);
 lean_dec(x_21);
-x_24 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_24 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_25 = lean_string_append(x_23, x_24);
 x_26 = lean_string_append(x_25, x_19);
 lean_dec(x_19);
@ -7511,7 +7637,7 @@ x_32 = l_Lean_Name_toStringWithSep___main(x_31, x_1);
 x_33 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_34 = lean_string_append(x_33, x_32);
 lean_dec(x_32);
-x_35 = l_Lean_registerTagAttribute___lambda__4___closed__5;
+x_35 = l_Lean_registerTagAttribute___lambda__4___closed__4;
 x_36 = lean_string_append(x_34, x_35);
 x_37 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_37, 0, x_36);
@ -8550,6 +8676,10 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Syntax(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_AttributeApplicationTime_hasBeq___closed__1 = _init_l_Lean_AttributeApplicationTime_hasBeq___closed__1();
+lean_mark_persistent(l_Lean_AttributeApplicationTime_hasBeq___closed__1);
+l_Lean_AttributeApplicationTime_hasBeq = _init_l_Lean_AttributeApplicationTime_hasBeq();
+lean_mark_persistent(l_Lean_AttributeApplicationTime_hasBeq);
 l_Lean_AttributeImpl_inhabited___lambda__2___closed__1 = _init_l_Lean_AttributeImpl_inhabited___lambda__2___closed__1();
 lean_mark_persistent(l_Lean_AttributeImpl_inhabited___lambda__2___closed__1);
 l_Lean_AttributeImpl_inhabited___lambda__2___closed__2 = _init_l_Lean_AttributeImpl_inhabited___lambda__2___closed__2();
--- a/stage0/stdlib/Init/Lean/Class.c
+++ b/stage0/stdlib/Init/Lean/Class.c
@ -194,7 +194,6 @@ lean_object* l_Lean_mkClassExtension___closed__2;
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l___private_Init_Lean_Class_1__checkOutParam(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Class_1__checkOutParam___main(lean_object*, lean_object*, lean_object*);
-uint8_t l_Lean_Syntax_isMissing(lean_object*);
 lean_object* l_HashMapImp_moveEntries___main___at_Lean_ClassState_addEntry___spec__9(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Class_2__consumeNLambdas___main(lean_object*, lean_object*);
 lean_object* l_HashMapImp_contains___at_Lean_isClass___spec__2___boxed(lean_object*, lean_object*);
@ -207,6 +206,7 @@ lean_object* l_PersistentHashMap_insert___at_Lean_ClassState_addEntry___spec__2(
 uint8_t l_PersistentHashMap_contains___at_Lean_isClass___spec__3(lean_object*, lean_object*);
 lean_object* l_Lean_registerTagAttribute___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_classExtension___closed__4;
+uint8_t l_Lean_Syntax_hasArgs(lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 uint8_t l_USize_decLe(size_t, size_t);
 lean_object* l_Lean_registerClassAttr___closed__3;
@ -6484,7 +6484,7 @@ lean_object* _init_l_Lean_registerClassAttr___lambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("invalid attribute 'class', unexpected argument");
+x_1 = lean_mk_string("invalid attribute 'class', must be persistent");
 return x_1;
 }
 }
@ -6492,7 +6492,7 @@ lean_object* _init_l_Lean_registerClassAttr___lambda__1___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("invalid attribute 'class', must be persistent");
+x_1 = lean_mk_string("invalid attribute 'class', unexpected argument");
 return x_1;
 }
 }
@ -6500,9 +6500,11 @@ lean_object* l_Lean_registerClassAttr___lambda__1(lean_object* x_1, lean_object*
 _start:
 {
 uint8_t x_6; 
-x_6 = l_Lean_Syntax_isMissing(x_3);
+x_6 = l_Lean_Syntax_hasArgs(x_3);
 if (x_6 == 0)
 {
+if (x_4 == 0)
+{
 lean_object* x_7; lean_object* x_8; 
 lean_dec(x_2);
 lean_dec(x_1);
@ -6514,28 +6516,26 @@ return x_8;
 }
 else
 {
-if (x_4 == 0)
-{
 lean_object* x_9; lean_object* x_10; 
-lean_dec(x_2);
-lean_dec(x_1);
-x_9 = l_Lean_registerClassAttr___lambda__1___closed__2;
-x_10 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_10, 0, x_9);
-lean_ctor_set(x_10, 1, x_5);
+x_9 = l_Lean_addClass(x_1, x_2);
+x_10 = l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(x_9, x_5);
+lean_dec(x_9);
 return x_10;
 }
+}
 else
 {
 lean_object* x_11; lean_object* x_12; 
-x_11 = l_Lean_addClass(x_1, x_2);
-x_12 = l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(x_11, x_5);
-lean_dec(x_11);
+lean_dec(x_2);
+lean_dec(x_1);
+x_11 = l_Lean_registerClassAttr___lambda__1___closed__2;
+x_12 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_12, 0, x_11);
+lean_ctor_set(x_12, 1, x_5);
 return x_12;
 }
 }
 }
-}
 lean_object* _init_l_Lean_registerClassAttr___closed__1() {
 _start:
 {
--- a/stage0/stdlib/Init/Lean/Compiler/IR/Checker.c
+++ b/stage0/stdlib/Init/Lean/Compiler/IR/Checker.c
@ -41,6 +41,7 @@ lean_object* l_Lean_IR_Decl_name(lean_object*);
 lean_object* l_RBNode_findCore___main___at_Lean_IR_Checker_markIndex___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_IR_Checker_checkVar___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_Checker_checkVar___closed__1;
+extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__3;
 lean_object* l_Array_iterateMAux___main___at_Lean_IR_Checker_checkDecl___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_LocalContext_getType(lean_object*, lean_object*);
 lean_object* l_Lean_IR_Checker_getDecl(lean_object*, lean_object*, lean_object*);
@ -118,7 +119,6 @@ lean_object* l_Array_iterateMAux___main___at_Lean_IR_Checker_withParams___spec__
 lean_object* l_Lean_IR_Checker_checkFullApp___closed__3;
 lean_object* l_Lean_IR_Checker_checkScalarVar(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_Checker_checkFnBody___main(lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__4;
 lean_object* l_Lean_IR_Checker_checkType___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_Checker_checkDecl(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_Decl_params(lean_object*);
@ -1336,7 +1336,7 @@ x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_1);
 x_28 = l_Lean_IR_Checker_checkFullApp___closed__1;
 x_29 = lean_string_append(x_28, x_27);
 lean_dec(x_27);
-x_30 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_30 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_31 = lean_string_append(x_29, x_30);
 x_32 = l_Nat_repr(x_22);
 x_33 = lean_string_append(x_31, x_32);
@ -1385,7 +1385,7 @@ x_48 = l_Lean_Name_toStringWithSep___main(x_47, x_1);
 x_49 = l_Lean_IR_Checker_checkFullApp___closed__1;
 x_50 = lean_string_append(x_49, x_48);
 lean_dec(x_48);
-x_51 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_51 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_52 = lean_string_append(x_50, x_51);
 x_53 = l_Nat_repr(x_43);
 x_54 = lean_string_append(x_52, x_53);
@ -1444,7 +1444,7 @@ x_72 = l_Lean_Name_toStringWithSep___main(x_71, x_1);
 x_73 = l_Lean_IR_Checker_checkFullApp___closed__1;
 x_74 = lean_string_append(x_73, x_72);
 lean_dec(x_72);
-x_75 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_75 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_76 = lean_string_append(x_74, x_75);
 x_77 = l_Nat_repr(x_67);
 x_78 = lean_string_append(x_76, x_77);
--- a/stage0/stdlib/Init/Lean/Compiler/InlineAttrs.c
+++ b/stage0/stdlib/Init/Lean/Compiler/InlineAttrs.c
@ -93,6 +93,7 @@ lean_object* l_Lean_Compiler_mkInlineAttrs___closed__17;
 lean_object* l_Lean_Compiler_mkInlineAttrs___closed__8;
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_checkIsDefinition(lean_object*, lean_object*);
+extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__2;
 lean_object* l_Lean_Compiler_mkInlineAttrs___closed__9;
 uint8_t lean_has_inline_attribute(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_mkInlineAttrs___closed__27;
@ -108,7 +109,6 @@ extern lean_object* l_Lean_EnumAttributes_Inhabited___closed__1;
 lean_object* l_Lean_Compiler_mkInlineAttrs___closed__1;
 lean_object* l_Lean_registerTagAttribute___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
-extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
 uint8_t l_Lean_Name_isInternal___main(lean_object*);
 lean_object* l_Lean_Compiler_mkInlineAttrs___closed__19;
 uint8_t l___private_Init_Lean_Compiler_InlineAttrs_1__hasInlineAttrAux(lean_object*, uint8_t, lean_object*);
@ -1264,7 +1264,7 @@ x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_1);
 x_12 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_13 = lean_string_append(x_12, x_11);
 lean_dec(x_11);
-x_14 = l_Lean_registerTagAttribute___lambda__4___closed__3;
+x_14 = l_Lean_registerTagAttribute___lambda__4___closed__2;
 x_15 = lean_string_append(x_13, x_14);
 x_16 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_16, 0, x_15);
@ -1296,7 +1296,7 @@ x_22 = l_Lean_Name_toStringWithSep___main(x_21, x_1);
 x_23 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_24 = lean_string_append(x_23, x_22);
 lean_dec(x_22);
-x_25 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_25 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_26 = lean_string_append(x_24, x_25);
 x_27 = lean_string_append(x_26, x_20);
 lean_dec(x_20);
@ -1334,7 +1334,7 @@ x_34 = l_Lean_Name_toStringWithSep___main(x_33, x_1);
 x_35 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_36 = lean_string_append(x_35, x_34);
 lean_dec(x_34);
-x_37 = l_Lean_registerTagAttribute___lambda__4___closed__5;
+x_37 = l_Lean_registerTagAttribute___lambda__4___closed__4;
 x_38 = lean_string_append(x_36, x_37);
 x_39 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_39, 0, x_38);
--- a/stage0/stdlib/Init/Lean/Compiler/Specialize.c
+++ b/stage0/stdlib/Init/Lean/Compiler/Specialize.c
@ -166,6 +166,7 @@ lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Compi
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
 size_t l_USize_land(size_t, size_t);
 lean_object* l_Lean_Compiler_SpecializeAttributeKind_beq___boxed(lean_object*, lean_object*);
+extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__2;
 lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Compiler_SpecState_addEntry___spec__5(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_cache_specialization(lean_object*, lean_object*, lean_object*);
@ -189,7 +190,6 @@ uint8_t lean_has_nospecialize_attribute(lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 uint8_t l_USize_decLe(size_t, size_t);
-extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
 lean_object* l_Lean_SMap_find_x3f___at_Lean_Compiler_getSpecializationInfo___spec__1(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_Compiler_getCachedSpecialization___spec__2(lean_object*, lean_object*);
 uint8_t l_Lean_Name_isInternal___main(lean_object*);
@ -1345,7 +1345,7 @@ x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_1);
 x_12 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_13 = lean_string_append(x_12, x_11);
 lean_dec(x_11);
-x_14 = l_Lean_registerTagAttribute___lambda__4___closed__3;
+x_14 = l_Lean_registerTagAttribute___lambda__4___closed__2;
 x_15 = lean_string_append(x_13, x_14);
 x_16 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_16, 0, x_15);
@ -1377,7 +1377,7 @@ x_22 = l_Lean_Name_toStringWithSep___main(x_21, x_1);
 x_23 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_24 = lean_string_append(x_23, x_22);
 lean_dec(x_22);
-x_25 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_25 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_26 = lean_string_append(x_24, x_25);
 x_27 = lean_string_append(x_26, x_20);
 lean_dec(x_20);
@ -1415,7 +1415,7 @@ x_34 = l_Lean_Name_toStringWithSep___main(x_33, x_1);
 x_35 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_36 = lean_string_append(x_35, x_34);
 lean_dec(x_34);
-x_37 = l_Lean_registerTagAttribute___lambda__4___closed__5;
+x_37 = l_Lean_registerTagAttribute___lambda__4___closed__4;
 x_38 = lean_string_append(x_36, x_37);
 x_39 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_39, 0, x_38);
--- a/stage0/stdlib/Init/Lean/Elab/Command.c
+++ b/stage0/stdlib/Init/Lean/Elab/Command.c
--- a/stage0/stdlib/Init/Lean/Elab/DeclModifiers.c
+++ b/stage0/stdlib/Init/Lean/Elab/DeclModifiers.c
--- a/stage0/stdlib/Init/Lean/Elab/Declaration.c
+++ b/stage0/stdlib/Init/Lean/Elab/Declaration.c
--- a/stage0/stdlib/Init/Lean/Elab/Definition.c
+++ b/stage0/stdlib/Init/Lean/Elab/Definition.c
--- a/stage0/stdlib/Init/Lean/Elab/ElabStrategyAttrs.c
+++ b/stage0/stdlib/Init/Lean/Elab/ElabStrategyAttrs.c
@ -72,6 +72,7 @@ lean_object* l_Array_binSearchAux___main___at_Lean_getElaboratorStrategy___spec_
 lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__6;
 lean_object* l_RBNode_find___main___at_Lean_getElaboratorStrategy___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__2;
 lean_object* l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___lambda__2(lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
@ -81,7 +82,6 @@ lean_object* l_Array_qsortAux___main___at_Lean_mkElaboratorStrategyAttrs___spec_
 lean_object* l_Lean_registerTagAttribute___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__16;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
-extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
 lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerEnumAttributes___rarg___closed__1;
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__4;
@ -1132,7 +1132,7 @@ x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_1);
 x_12 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_13 = lean_string_append(x_12, x_11);
 lean_dec(x_11);
-x_14 = l_Lean_registerTagAttribute___lambda__4___closed__3;
+x_14 = l_Lean_registerTagAttribute___lambda__4___closed__2;
 x_15 = lean_string_append(x_13, x_14);
 x_16 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_16, 0, x_15);
@ -1164,7 +1164,7 @@ x_22 = l_Lean_Name_toStringWithSep___main(x_21, x_1);
 x_23 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_24 = lean_string_append(x_23, x_22);
 lean_dec(x_22);
-x_25 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_25 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_26 = lean_string_append(x_24, x_25);
 x_27 = lean_string_append(x_26, x_20);
 lean_dec(x_20);
@ -1202,7 +1202,7 @@ x_34 = l_Lean_Name_toStringWithSep___main(x_33, x_1);
 x_35 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_36 = lean_string_append(x_35, x_34);
 lean_dec(x_34);
-x_37 = l_Lean_registerTagAttribute___lambda__4___closed__5;
+x_37 = l_Lean_registerTagAttribute___lambda__4___closed__4;
 x_38 = lean_string_append(x_36, x_37);
 x_39 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_39, 0, x_38);
--- a/stage0/stdlib/Init/Lean/Elab/Frontend.c
+++ b/stage0/stdlib/Init/Lean/Elab/Frontend.c
--- a/stage0/stdlib/Init/Lean/Elab/Term.c
+++ b/stage0/stdlib/Init/Lean/Elab/Term.c
@ -95,6 +95,7 @@ extern size_t l_PersistentHashMap_insertAux___main___rarg___closed__2;
 lean_object* l_Lean_Elab_Term_throwUnexpectedSyntax___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_Term_3__addMacroStack___spec__1___closed__1;
 lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_levelMVarToParam___closed__1;
 lean_object* l_Lean_Elab_Term_elabParen(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNum___closed__2;
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
@ -108,6 +109,7 @@ lean_object* l___private_Init_Lean_Elab_Term_22__resolveLocalNameAux___main(lean
 lean_object* l_Lean_Elab_Term_elabArrayLit___closed__2;
 extern lean_object* l_Lean_Parser_Term_type___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_throwUnexpectedSyntax___rarg___closed__2;
+uint8_t l_List_elem___main___at_Lean_addAliasEntry___spec__18(lean_object*, lean_object*);
 extern lean_object* l_Prod_HasRepr___rarg___closed__1;
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Term_6__fromMetaState___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_stxInh;
@ -138,6 +140,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBadCDot(lean_object*);
 lean_object* l_Lean_Elab_Term_unfoldDefinition_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* l_List_filterAuxM___main___at_Lean_Elab_Term_synthesizeUsingDefault___spec__1___lambda__1___closed__3;
+lean_object* l_Lean_Elab_Term_mkForallUsedOnly___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_ref_get(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__5;
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___closed__6;
@ -164,6 +167,7 @@ lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_Elab_Term_elabChar___closed__4;
 lean_object* l_List_find_x3f___main___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_resetSynthInstanceCache(lean_object*);
+lean_object* l_Lean_Elab_Term_mkForallUsedOnly(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_inferType___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerAttribute(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_14__synthesizePendingInstMVar___lambda__1___closed__1;
@ -289,6 +293,7 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withMVarContext(lean_object*);
 extern lean_object* l_Lean_Name_appendIndexAfter___closed__1;
 lean_object* l_Lean_Elab_Term_termElabAttribute___closed__4;
+lean_object* l_Lean_Elab_Term_levelMVarToParam(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_observing(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__4(lean_object*, lean_object*, lean_object*);
@ -308,6 +313,7 @@ lean_object* l_Lean_Elab_Term_decLevel_x3f(lean_object*, lean_object*, lean_obje
 extern lean_object* l_Lean_numLitKind;
 lean_object* l_Lean_Elab_Term_elabTerm___closed__6;
 lean_object* l___private_Init_Lean_Elab_Term_25__mkConsts(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_MetavarContext_levelMVarToParam(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabChar___closed__2;
 lean_object* l_Lean_Elab_Term_mkLambda___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getLevel(lean_object*, lean_object*, lean_object*, lean_object*);
@ -333,6 +339,7 @@ lean_object* l_Lean_Elab_mkMessageCore(lean_object*, lean_object*, lean_object*,
 lean_object* l_Lean_Elab_Term_mkHole___boxed(lean_object*);
 lean_object* l_Lean_Elab_Term_withMacroExpansion___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__3;
+lean_object* l_Lean_Elab_Term_levelMVarToParam___closed__2;
 lean_object* l_Lean_Elab_Term_elabStr___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabParen(lean_object*);
 lean_object* l_Lean_Elab_Term_mkConst___closed__2;
@ -348,6 +355,7 @@ lean_object* l_Lean_Elab_Term_mkInstMVar(lean_object*, lean_object*, lean_object
 lean_object* l___private_Init_Lean_Elab_Term_20__mkPairsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__6;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_setTraceState___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
@ -358,6 +366,7 @@ lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkConst___closed__4;
 lean_object* l_List_forM___main___at___private_Init_Lean_Elab_Term_18__reportStuckSyntheticMVars___spec__1___lambda__1___closed__2;
 lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Meta_mkForallUsedOnly(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Term_6__fromMetaState___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withNode___rarg___closed__1;
@ -628,6 +637,7 @@ lean_object* lean_io_ref_reset(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_unfoldDefinition_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkExplicitBinder(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabSort(lean_object*, lean_object*, lean_object*);
+uint8_t l_Lean_Elab_Term_levelMVarToParam___lambda__1(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_17__synthesizeSyntheticMVarsStep___closed__7;
 lean_object* l___private_Init_Lean_Elab_Term_14__synthesizePendingInstMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -7836,6 +7846,174 @@ lean_dec(x_1);
 return x_6;
 }
 }
+lean_object* l_Lean_Elab_Term_mkForallUsedOnly(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; uint8_t x_7; 
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+x_7 = !lean_is_exclusive(x_6);
+if (x_7 == 0)
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = lean_ctor_get(x_6, 4);
+x_9 = lean_ctor_get(x_4, 0);
+lean_inc(x_9);
+x_10 = l_Lean_TraceState_Inhabited___closed__1;
+lean_ctor_set(x_6, 4, x_10);
+x_11 = l_Lean_Meta_mkForallUsedOnly(x_2, x_3, x_9, x_6);
+if (lean_obj_tag(x_11) == 0)
+{
+uint8_t x_12; 
+x_12 = !lean_is_exclusive(x_11);
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; 
+x_13 = lean_ctor_get(x_11, 1);
+x_14 = l___private_Init_Lean_Elab_Term_6__fromMetaState(x_1, x_4, x_5, x_13, x_8);
+lean_ctor_set(x_11, 1, x_14);
+return x_11;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_15 = lean_ctor_get(x_11, 0);
+x_16 = lean_ctor_get(x_11, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_11);
+x_17 = l___private_Init_Lean_Elab_Term_6__fromMetaState(x_1, x_4, x_5, x_16, x_8);
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_15);
+lean_ctor_set(x_18, 1, x_17);
+return x_18;
+}
+}
+else
+{
+uint8_t x_19; 
+x_19 = !lean_is_exclusive(x_11);
+if (x_19 == 0)
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_20 = lean_ctor_get(x_11, 0);
+x_21 = lean_ctor_get(x_11, 1);
+lean_inc(x_4);
+x_22 = l___private_Init_Lean_Elab_Term_5__fromMetaException(x_4, x_1, x_20);
+x_23 = l___private_Init_Lean_Elab_Term_6__fromMetaState(x_1, x_4, x_5, x_21, x_8);
+lean_ctor_set(x_11, 1, x_23);
+lean_ctor_set(x_11, 0, x_22);
+return x_11;
+}
+else
+{
+lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_24 = lean_ctor_get(x_11, 0);
+x_25 = lean_ctor_get(x_11, 1);
+lean_inc(x_25);
+lean_inc(x_24);
+lean_dec(x_11);
+lean_inc(x_4);
+x_26 = l___private_Init_Lean_Elab_Term_5__fromMetaException(x_4, x_1, x_24);
+x_27 = l___private_Init_Lean_Elab_Term_6__fromMetaState(x_1, x_4, x_5, x_25, x_8);
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_26);
+lean_ctor_set(x_28, 1, x_27);
+return x_28;
+}
+}
+}
+else
+{
+lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; 
+x_29 = lean_ctor_get(x_6, 0);
+x_30 = lean_ctor_get(x_6, 1);
+x_31 = lean_ctor_get(x_6, 2);
+x_32 = lean_ctor_get(x_6, 3);
+x_33 = lean_ctor_get(x_6, 4);
+x_34 = lean_ctor_get(x_6, 5);
+lean_inc(x_34);
+lean_inc(x_33);
+lean_inc(x_32);
+lean_inc(x_31);
+lean_inc(x_30);
+lean_inc(x_29);
+lean_dec(x_6);
+x_35 = lean_ctor_get(x_4, 0);
+lean_inc(x_35);
+x_36 = l_Lean_TraceState_Inhabited___closed__1;
+x_37 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_37, 0, x_29);
+lean_ctor_set(x_37, 1, x_30);
+lean_ctor_set(x_37, 2, x_31);
+lean_ctor_set(x_37, 3, x_32);
+lean_ctor_set(x_37, 4, x_36);
+lean_ctor_set(x_37, 5, x_34);
+x_38 = l_Lean_Meta_mkForallUsedOnly(x_2, x_3, x_35, x_37);
+if (lean_obj_tag(x_38) == 0)
+{
+lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_39 = lean_ctor_get(x_38, 0);
+lean_inc(x_39);
+x_40 = lean_ctor_get(x_38, 1);
+lean_inc(x_40);
+if (lean_is_exclusive(x_38)) {
+ lean_ctor_release(x_38, 0);
+ lean_ctor_release(x_38, 1);
+ x_41 = x_38;
+} else {
+ lean_dec_ref(x_38);
+ x_41 = lean_box(0);
+}
+x_42 = l___private_Init_Lean_Elab_Term_6__fromMetaState(x_1, x_4, x_5, x_40, x_33);
+if (lean_is_scalar(x_41)) {
+ x_43 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_43 = x_41;
+}
+lean_ctor_set(x_43, 0, x_39);
+lean_ctor_set(x_43, 1, x_42);
+return x_43;
+}
+else
+{
+lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_44 = lean_ctor_get(x_38, 0);
+lean_inc(x_44);
+x_45 = lean_ctor_get(x_38, 1);
+lean_inc(x_45);
+if (lean_is_exclusive(x_38)) {
+ lean_ctor_release(x_38, 0);
+ lean_ctor_release(x_38, 1);
+ x_46 = x_38;
+} else {
+ lean_dec_ref(x_38);
+ x_46 = lean_box(0);
+}
+lean_inc(x_4);
+x_47 = l___private_Init_Lean_Elab_Term_5__fromMetaException(x_4, x_1, x_44);
+x_48 = l___private_Init_Lean_Elab_Term_6__fromMetaState(x_1, x_4, x_5, x_45, x_33);
+if (lean_is_scalar(x_46)) {
+ x_49 = lean_alloc_ctor(1, 2, 0);
+} else {
+ x_49 = x_46;
+}
+lean_ctor_set(x_49, 0, x_47);
+lean_ctor_set(x_49, 1, x_48);
+return x_49;
+}
+}
+}
+}
+lean_object* l_Lean_Elab_Term_mkForallUsedOnly___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = l_Lean_Elab_Term_mkForallUsedOnly(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_1);
+return x_6;
+}
+}
 lean_object* l_Lean_Elab_Term_mkLambda(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
@ -9359,6 +9537,270 @@ lean_ctor_set(x_18, 1, x_16);
 return x_18;
 }
 }
+uint8_t l_Lean_Elab_Term_levelMVarToParam___lambda__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; uint8_t x_4; 
+x_3 = lean_ctor_get(x_1, 5);
+x_4 = l_List_elem___main___at_Lean_addAliasEntry___spec__18(x_2, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_levelMVarToParam___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("u");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_levelMVarToParam___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Elab_Term_levelMVarToParam___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Elab_Term_levelMVarToParam(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; uint8_t x_5; 
+x_4 = l_Lean_Elab_Term_getMCtx___rarg(x_3);
+x_5 = !lean_is_exclusive(x_4);
+if (x_5 == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; 
+x_6 = lean_ctor_get(x_4, 0);
+x_7 = lean_ctor_get(x_4, 1);
+x_8 = lean_alloc_closure((void*)(l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed), 2, 1);
+lean_closure_set(x_8, 0, x_2);
+x_9 = l_Lean_Elab_Term_levelMVarToParam___closed__2;
+x_10 = lean_unsigned_to_nat(1u);
+x_11 = l_Lean_MetavarContext_levelMVarToParam(x_6, x_8, x_1, x_9, x_10);
+x_12 = !lean_is_exclusive(x_7);
+if (x_12 == 0)
+{
+lean_object* x_13; uint8_t x_14; 
+x_13 = lean_ctor_get(x_7, 0);
+x_14 = !lean_is_exclusive(x_13);
+if (x_14 == 0)
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = lean_ctor_get(x_13, 1);
+lean_dec(x_15);
+x_16 = lean_ctor_get(x_11, 0);
+lean_inc(x_16);
+lean_ctor_set(x_13, 1, x_16);
+x_17 = lean_ctor_get(x_11, 3);
+lean_inc(x_17);
+lean_dec(x_11);
+lean_ctor_set(x_4, 0, x_17);
+return x_4;
+}
+else
+{
+lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_18 = lean_ctor_get(x_13, 0);
+x_19 = lean_ctor_get(x_13, 2);
+x_20 = lean_ctor_get(x_13, 3);
+x_21 = lean_ctor_get(x_13, 4);
+x_22 = lean_ctor_get(x_13, 5);
+lean_inc(x_22);
+lean_inc(x_21);
+lean_inc(x_20);
+lean_inc(x_19);
+lean_inc(x_18);
+lean_dec(x_13);
+x_23 = lean_ctor_get(x_11, 0);
+lean_inc(x_23);
+x_24 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_24, 0, x_18);
+lean_ctor_set(x_24, 1, x_23);
+lean_ctor_set(x_24, 2, x_19);
+lean_ctor_set(x_24, 3, x_20);
+lean_ctor_set(x_24, 4, x_21);
+lean_ctor_set(x_24, 5, x_22);
+lean_ctor_set(x_7, 0, x_24);
+x_25 = lean_ctor_get(x_11, 3);
+lean_inc(x_25);
+lean_dec(x_11);
+lean_ctor_set(x_4, 0, x_25);
+return x_4;
+}
+}
+else
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; 
+x_26 = lean_ctor_get(x_7, 0);
+x_27 = lean_ctor_get(x_7, 1);
+x_28 = lean_ctor_get(x_7, 2);
+x_29 = lean_ctor_get(x_7, 3);
+x_30 = lean_ctor_get(x_7, 4);
+x_31 = lean_ctor_get(x_7, 5);
+lean_inc(x_31);
+lean_inc(x_30);
+lean_inc(x_29);
+lean_inc(x_28);
+lean_inc(x_27);
+lean_inc(x_26);
+lean_dec(x_7);
+x_32 = lean_ctor_get(x_26, 0);
+lean_inc(x_32);
+x_33 = lean_ctor_get(x_26, 2);
+lean_inc(x_33);
+x_34 = lean_ctor_get(x_26, 3);
+lean_inc(x_34);
+x_35 = lean_ctor_get(x_26, 4);
+lean_inc(x_35);
+x_36 = lean_ctor_get(x_26, 5);
+lean_inc(x_36);
+if (lean_is_exclusive(x_26)) {
+ lean_ctor_release(x_26, 0);
+ lean_ctor_release(x_26, 1);
+ lean_ctor_release(x_26, 2);
+ lean_ctor_release(x_26, 3);
+ lean_ctor_release(x_26, 4);
+ lean_ctor_release(x_26, 5);
+ x_37 = x_26;
+} else {
+ lean_dec_ref(x_26);
+ x_37 = lean_box(0);
+}
+x_38 = lean_ctor_get(x_11, 0);
+lean_inc(x_38);
+if (lean_is_scalar(x_37)) {
+ x_39 = lean_alloc_ctor(0, 6, 0);
+} else {
+ x_39 = x_37;
+}
+lean_ctor_set(x_39, 0, x_32);
+lean_ctor_set(x_39, 1, x_38);
+lean_ctor_set(x_39, 2, x_33);
+lean_ctor_set(x_39, 3, x_34);
+lean_ctor_set(x_39, 4, x_35);
+lean_ctor_set(x_39, 5, x_36);
+x_40 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_40, 0, x_39);
+lean_ctor_set(x_40, 1, x_27);
+lean_ctor_set(x_40, 2, x_28);
+lean_ctor_set(x_40, 3, x_29);
+lean_ctor_set(x_40, 4, x_30);
+lean_ctor_set(x_40, 5, x_31);
+x_41 = lean_ctor_get(x_11, 3);
+lean_inc(x_41);
+lean_dec(x_11);
+lean_ctor_set(x_4, 1, x_40);
+lean_ctor_set(x_4, 0, x_41);
+return x_4;
+}
+}
+else
+{
+lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; 
+x_42 = lean_ctor_get(x_4, 0);
+x_43 = lean_ctor_get(x_4, 1);
+lean_inc(x_43);
+lean_inc(x_42);
+lean_dec(x_4);
+x_44 = lean_alloc_closure((void*)(l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed), 2, 1);
+lean_closure_set(x_44, 0, x_2);
+x_45 = l_Lean_Elab_Term_levelMVarToParam___closed__2;
+x_46 = lean_unsigned_to_nat(1u);
+x_47 = l_Lean_MetavarContext_levelMVarToParam(x_42, x_44, x_1, x_45, x_46);
+x_48 = lean_ctor_get(x_43, 0);
+lean_inc(x_48);
+x_49 = lean_ctor_get(x_43, 1);
+lean_inc(x_49);
+x_50 = lean_ctor_get(x_43, 2);
+lean_inc(x_50);
+x_51 = lean_ctor_get(x_43, 3);
+lean_inc(x_51);
+x_52 = lean_ctor_get(x_43, 4);
+lean_inc(x_52);
+x_53 = lean_ctor_get(x_43, 5);
+lean_inc(x_53);
+if (lean_is_exclusive(x_43)) {
+ lean_ctor_release(x_43, 0);
+ lean_ctor_release(x_43, 1);
+ lean_ctor_release(x_43, 2);
+ lean_ctor_release(x_43, 3);
+ lean_ctor_release(x_43, 4);
+ lean_ctor_release(x_43, 5);
+ x_54 = x_43;
+} else {
+ lean_dec_ref(x_43);
+ x_54 = lean_box(0);
+}
+x_55 = lean_ctor_get(x_48, 0);
+lean_inc(x_55);
+x_56 = lean_ctor_get(x_48, 2);
+lean_inc(x_56);
+x_57 = lean_ctor_get(x_48, 3);
+lean_inc(x_57);
+x_58 = lean_ctor_get(x_48, 4);
+lean_inc(x_58);
+x_59 = lean_ctor_get(x_48, 5);
+lean_inc(x_59);
+if (lean_is_exclusive(x_48)) {
+ lean_ctor_release(x_48, 0);
+ lean_ctor_release(x_48, 1);
+ lean_ctor_release(x_48, 2);
+ lean_ctor_release(x_48, 3);
+ lean_ctor_release(x_48, 4);
+ lean_ctor_release(x_48, 5);
+ x_60 = x_48;
+} else {
+ lean_dec_ref(x_48);
+ x_60 = lean_box(0);
+}
+x_61 = lean_ctor_get(x_47, 0);
+lean_inc(x_61);
+if (lean_is_scalar(x_60)) {
+ x_62 = lean_alloc_ctor(0, 6, 0);
+} else {
+ x_62 = x_60;
+}
+lean_ctor_set(x_62, 0, x_55);
+lean_ctor_set(x_62, 1, x_61);
+lean_ctor_set(x_62, 2, x_56);
+lean_ctor_set(x_62, 3, x_57);
+lean_ctor_set(x_62, 4, x_58);
+lean_ctor_set(x_62, 5, x_59);
+if (lean_is_scalar(x_54)) {
+ x_63 = lean_alloc_ctor(0, 6, 0);
+} else {
+ x_63 = x_54;
+}
+lean_ctor_set(x_63, 0, x_62);
+lean_ctor_set(x_63, 1, x_49);
+lean_ctor_set(x_63, 2, x_50);
+lean_ctor_set(x_63, 3, x_51);
+lean_ctor_set(x_63, 4, x_52);
+lean_ctor_set(x_63, 5, x_53);
+x_64 = lean_ctor_get(x_47, 3);
+lean_inc(x_64);
+lean_dec(x_47);
+x_65 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_65, 0, x_64);
+lean_ctor_set(x_65, 1, x_63);
+return x_65;
+}
+}
+}
+lean_object* l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = l_Lean_Elab_Term_levelMVarToParam___lambda__1(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
 lean_object* _init_l_Lean_Elab_Term_mkFreshAnonymousName___rarg___closed__1() {
 _start:
 {
@ -22365,6 +22807,10 @@ l_Lean_Elab_Term_mkExplicitBinder___closed__5 = _init_l_Lean_Elab_Term_mkExplici
 lean_mark_persistent(l_Lean_Elab_Term_mkExplicitBinder___closed__5);
 l_Lean_Elab_Term_mkExplicitBinder___closed__6 = _init_l_Lean_Elab_Term_mkExplicitBinder___closed__6();
 lean_mark_persistent(l_Lean_Elab_Term_mkExplicitBinder___closed__6);
+l_Lean_Elab_Term_levelMVarToParam___closed__1 = _init_l_Lean_Elab_Term_levelMVarToParam___closed__1();
+lean_mark_persistent(l_Lean_Elab_Term_levelMVarToParam___closed__1);
+l_Lean_Elab_Term_levelMVarToParam___closed__2 = _init_l_Lean_Elab_Term_levelMVarToParam___closed__2();
+lean_mark_persistent(l_Lean_Elab_Term_levelMVarToParam___closed__2);
 l_Lean_Elab_Term_mkFreshAnonymousName___rarg___closed__1 = _init_l_Lean_Elab_Term_mkFreshAnonymousName___rarg___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_mkFreshAnonymousName___rarg___closed__1);
 l_Lean_Elab_Term_mkFreshAnonymousName___rarg___closed__2 = _init_l_Lean_Elab_Term_mkFreshAnonymousName___rarg___closed__2();
--- a/stage0/stdlib/Init/Lean/Elab/Util.c
+++ b/stage0/stdlib/Init/Lean/Elab/Util.c
@ -839,7 +839,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("' `");
+x_1 = lean_mk_string("', `");
 return x_1;
 }
 }
--- a/stage0/stdlib/Init/Lean/Expr.c
+++ b/stage0/stdlib/Init/Lean/Expr.c
@ -7452,7 +7452,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(758u);
+x_2 = lean_unsigned_to_nat(760u);
 x_3 = lean_unsigned_to_nat(18u);
 x_4 = l_Lean_Expr_appFn_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7494,7 +7494,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(767u);
+x_2 = lean_unsigned_to_nat(769u);
 x_3 = lean_unsigned_to_nat(18u);
 x_4 = l_Lean_Expr_constName_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7543,7 +7543,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(776u);
+x_2 = lean_unsigned_to_nat(778u);
 x_3 = lean_unsigned_to_nat(14u);
 x_4 = l_Lean_Expr_updateSort_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7600,7 +7600,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(793u);
+x_2 = lean_unsigned_to_nat(795u);
 x_3 = lean_unsigned_to_nat(17u);
 x_4 = l_Lean_Expr_updateMData_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7641,7 +7641,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(798u);
+x_2 = lean_unsigned_to_nat(800u);
 x_3 = lean_unsigned_to_nat(18u);
 x_4 = l_Lean_Expr_updateProj_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7692,7 +7692,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(807u);
+x_2 = lean_unsigned_to_nat(809u);
 x_3 = lean_unsigned_to_nat(21u);
 x_4 = l_Lean_Expr_updateForall_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7736,7 +7736,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(812u);
+x_2 = lean_unsigned_to_nat(814u);
 x_3 = lean_unsigned_to_nat(21u);
 x_4 = l_Lean_Expr_updateForall_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7790,7 +7790,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(821u);
+x_2 = lean_unsigned_to_nat(823u);
 x_3 = lean_unsigned_to_nat(17u);
 x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7834,7 +7834,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(826u);
+x_2 = lean_unsigned_to_nat(828u);
 x_3 = lean_unsigned_to_nat(17u);
 x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7878,7 +7878,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
-x_2 = lean_unsigned_to_nat(835u);
+x_2 = lean_unsigned_to_nat(837u);
 x_3 = lean_unsigned_to_nat(20u);
 x_4 = l_Lean_Expr_letName_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
--- a/stage0/stdlib/Init/Lean/Level.c
+++ b/stage0/stdlib/Init/Lean/Level.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Level
-// Imports: Init.Data.Option.Basic Init.Data.HashMap Init.Data.PersistentHashMap Init.Lean.Data.Name Init.Lean.Data.Format
+// Imports: Init.Data.Option.Basic Init.Data.HashMap Init.Data.PersistentHashMap Init.Data.HashSet Init.Data.PersistentHashSet Init.Lean.Data.Name Init.Lean.Data.Format
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -429,7 +429,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_Level_mkData___closed__2;
-x_2 = lean_unsigned_to_nat(45u);
+x_2 = lean_unsigned_to_nat(47u);
 x_3 = lean_unsigned_to_nat(33u);
 x_4 = l_Lean_Level_mkData___closed__3;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -1364,7 +1364,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_Level_mkData___closed__2;
-x_2 = lean_unsigned_to_nat(157u);
+x_2 = lean_unsigned_to_nat(159u);
 x_3 = lean_unsigned_to_nat(19u);
 x_4 = l_Lean_Level_mvarId_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -3798,7 +3798,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_Level_mkData___closed__2;
-x_2 = lean_unsigned_to_nat(401u);
+x_2 = lean_unsigned_to_nat(403u);
 x_3 = lean_unsigned_to_nat(16u);
 x_4 = l_Lean_Level_updateSucc_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -3847,7 +3847,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_Level_mkData___closed__2;
-x_2 = lean_unsigned_to_nat(410u);
+x_2 = lean_unsigned_to_nat(412u);
 x_3 = lean_unsigned_to_nat(19u);
 x_4 = l_Lean_Level_updateMax_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -3897,7 +3897,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_Level_mkData___closed__2;
-x_2 = lean_unsigned_to_nat(419u);
+x_2 = lean_unsigned_to_nat(421u);
 x_3 = lean_unsigned_to_nat(20u);
 x_4 = l_Lean_Level_updateIMax_x21___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -4056,6 +4056,8 @@ return x_2;
 lean_object* initialize_Init_Data_Option_Basic(lean_object*);
 lean_object* initialize_Init_Data_HashMap(lean_object*);
 lean_object* initialize_Init_Data_PersistentHashMap(lean_object*);
+lean_object* initialize_Init_Data_HashSet(lean_object*);
+lean_object* initialize_Init_Data_PersistentHashSet(lean_object*);
 lean_object* initialize_Init_Lean_Data_Name(lean_object*);
 lean_object* initialize_Init_Lean_Data_Format(lean_object*);
 static bool _G_initialized = false;
@ -4072,6 +4074,12 @@ lean_dec_ref(res);
 res = initialize_Init_Data_PersistentHashMap(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Data_HashSet(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Data_PersistentHashSet(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
--- a/stage0/stdlib/Init/Lean/Meta/Basic.c
+++ b/stage0/stdlib/Init/Lean/Meta/Basic.c
--- a/stage0/stdlib/Init/Lean/Meta/Instances.c
+++ b/stage0/stdlib/Init/Lean/Meta/Instances.c
@ -117,7 +117,6 @@ lean_object* l_Lean_Meta_DiscrTree_mkPath(lean_object*, lean_object*, lean_objec
 lean_object* l_Lean_Meta_forallMetaTelescopeReducing(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
-uint8_t l_Lean_Syntax_isMissing(lean_object*);
 lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Meta_addInstanceEntry___spec__6(lean_object*, size_t, size_t, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_Meta_addInstanceEntry___spec__3(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_Meta_registerInstanceAttr___lambda__1___closed__1;
@ -129,6 +128,7 @@ lean_object* l_Array_back___at_Lean_Meta_addInstanceEntry___spec__14___boxed(lea
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 lean_object* l_Lean_registerTagAttribute___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_DiscrTree_insertCore___rarg___closed__1;
+uint8_t l_Lean_Syntax_hasArgs(lean_object*);
 lean_object* l_Lean_Environment_getGlobalInstances(lean_object*);
 uint8_t l_USize_decLe(size_t, size_t);
 extern lean_object* l_Lean_Meta_DiscrTree_empty___closed__1;
@ -3350,7 +3350,7 @@ lean_object* _init_l_Lean_Meta_registerInstanceAttr___lambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("invalid attribute 'instance', unexpected argument");
+x_1 = lean_mk_string("invalid attribute 'instance', must be persistent");
 return x_1;
 }
 }
@ -3358,7 +3358,7 @@ lean_object* _init_l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("invalid attribute 'instance', must be persistent");
+x_1 = lean_mk_string("invalid attribute 'instance', unexpected argument");
 return x_1;
 }
 }
@ -3366,9 +3366,11 @@ lean_object* l_Lean_Meta_registerInstanceAttr___lambda__1(lean_object* x_1, lean
 _start:
 {
 uint8_t x_6; 
-x_6 = l_Lean_Syntax_isMissing(x_3);
+x_6 = l_Lean_Syntax_hasArgs(x_3);
 if (x_6 == 0)
 {
+if (x_4 == 0)
+{
 lean_object* x_7; lean_object* x_8; 
 lean_dec(x_2);
 lean_dec(x_1);
@ -3380,62 +3382,60 @@ return x_8;
 }
 else
 {
-if (x_4 == 0)
-{
 lean_object* x_9; lean_object* x_10; 
+lean_inc(x_2);
+x_9 = lean_add_instance_old(x_1, x_2);
+x_10 = l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(x_9, x_5);
+lean_dec(x_9);
+if (lean_obj_tag(x_10) == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_10, 1);
+lean_inc(x_12);
+lean_dec(x_10);
+x_13 = lean_add_instance(x_11, x_2, x_12);
+return x_13;
+}
+else
+{
+uint8_t x_14; 
 lean_dec(x_2);
-lean_dec(x_1);
-x_9 = l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2;
-x_10 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_10, 0, x_9);
-lean_ctor_set(x_10, 1, x_5);
+x_14 = !lean_is_exclusive(x_10);
+if (x_14 == 0)
+{
 return x_10;
 }
 else
 {
-lean_object* x_11; lean_object* x_12; 
-lean_inc(x_2);
-x_11 = lean_add_instance_old(x_1, x_2);
-x_12 = l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(x_11, x_5);
-lean_dec(x_11);
-if (lean_obj_tag(x_12) == 0)
-{
-lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
-lean_inc(x_14);
-lean_dec(x_12);
-x_15 = lean_add_instance(x_13, x_2, x_14);
-return x_15;
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = lean_ctor_get(x_10, 0);
+x_16 = lean_ctor_get(x_10, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_10);
+x_17 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_17, 0, x_15);
+lean_ctor_set(x_17, 1, x_16);
+return x_17;
+}
+}
+}
 }
 else
 {
-uint8_t x_16; 
+lean_object* x_18; lean_object* x_19; 
 lean_dec(x_2);
-x_16 = !lean_is_exclusive(x_12);
-if (x_16 == 0)
-{
-return x_12;
-}
-else
-{
-lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-x_17 = lean_ctor_get(x_12, 0);
-x_18 = lean_ctor_get(x_12, 1);
-lean_inc(x_18);
-lean_inc(x_17);
-lean_dec(x_12);
+lean_dec(x_1);
+x_18 = l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2;
 x_19 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_19, 0, x_17);
-lean_ctor_set(x_19, 1, x_18);
+lean_ctor_set(x_19, 0, x_18);
+lean_ctor_set(x_19, 1, x_5);
 return x_19;
 }
 }
 }
-}
-}
-}
 lean_object* _init_l_Lean_Meta_registerInstanceAttr___closed__1() {
 _start:
 {
--- a/stage0/stdlib/Init/Lean/MetavarContext.c
+++ b/stage0/stdlib/Init/Lean/MetavarContext.c
--- a/stage0/stdlib/Init/Lean/Parser/Parser.c
+++ b/stage0/stdlib/Init/Lean/Parser/Parser.c
--- a/stage0/stdlib/Init/Lean/ReducibilityAttrs.c
+++ b/stage0/stdlib/Init/Lean/ReducibilityAttrs.c
@ -76,6 +76,7 @@ lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkReducibilit
 lean_object* l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_ReducibilityStatus_inhabited;
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__2;
 lean_object* l_Lean_mkReducibilityAttrs___closed__4;
 lean_object* l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1___lambda__1(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
@ -87,7 +88,6 @@ lean_object* l_Lean_mkReducibilityAttrs___closed__7;
 lean_object* l_Lean_registerTagAttribute___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_RBNode_fold___main___at_Lean_mkReducibilityAttrs___spec__2___boxed(lean_object*, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
-extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
 lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerEnumAttributes___rarg___closed__1;
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__4;
@ -1135,7 +1135,7 @@ x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_1);
 x_12 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_13 = lean_string_append(x_12, x_11);
 lean_dec(x_11);
-x_14 = l_Lean_registerTagAttribute___lambda__4___closed__3;
+x_14 = l_Lean_registerTagAttribute___lambda__4___closed__2;
 x_15 = lean_string_append(x_13, x_14);
 x_16 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_16, 0, x_15);
@ -1167,7 +1167,7 @@ x_22 = l_Lean_Name_toStringWithSep___main(x_21, x_1);
 x_23 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_24 = lean_string_append(x_23, x_22);
 lean_dec(x_22);
-x_25 = l_Lean_registerTagAttribute___lambda__4___closed__4;
+x_25 = l_Lean_registerTagAttribute___lambda__4___closed__3;
 x_26 = lean_string_append(x_24, x_25);
 x_27 = lean_string_append(x_26, x_20);
 lean_dec(x_20);
@ -1205,7 +1205,7 @@ x_34 = l_Lean_Name_toStringWithSep___main(x_33, x_1);
 x_35 = l_Lean_registerTagAttribute___lambda__4___closed__1;
 x_36 = lean_string_append(x_35, x_34);
 lean_dec(x_34);
-x_37 = l_Lean_registerTagAttribute___lambda__4___closed__5;
+x_37 = l_Lean_registerTagAttribute___lambda__4___closed__4;
 x_38 = lean_string_append(x_36, x_37);
 x_39 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_39, 0, x_38);
--- a/stage0/stdlib/Init/Lean/Util/CollectLevelParams.c
+++ b/stage0/stdlib/Init/Lean/Util/CollectLevelParams.c