chore: update stage0

2019-12-12 09:00:02 -08:00 · 2019-12-12 09:00:02 -08:00 · 3974fee87c
commit 3974fee87c
parent a124461dca
24 changed files with 9328 additions and 6885 deletions
--- a/stage0/src/Init/Lean.lean
+++ b/stage0/src/Init/Lean.lean
@ -21,3 +21,4 @@ import Init.Lean.AuxRecursor
 import Init.Lean.Linter
 import Init.Lean.Meta
 import Init.Lean.Eval
+import Init.Lean.Structure
--- a/stage0/src/Init/Lean/Compiler/ExternAttr.lean
+++ b/stage0/src/Init/Lean/Compiler/ExternAttr.lean
@ -45,14 +45,14 @@ private partial def syntaxToExternEntries (a : Array Syntax) : Nat → List Exte
    | Syntax.ident _ _ backend _ =>
      let i := i + 1;
      if i == a.size then Except.error "string or identifier expected"
-      else match (a.get! i).isIdOrAtom with
+      else match (a.get! i).isIdOrAtom? with
        | some "adhoc"  => syntaxToExternEntries (i+1) (ExternEntry.adhoc backend :: entries)
        | some "inline" =>
          let i := i + 1;
-          match (a.get! i).isStrLit with
+          match (a.get! i).isStrLit? with
          | some pattern => syntaxToExternEntries (i+1) (ExternEntry.inline backend pattern :: entries)
          | none => Except.error "string literal expected"
-        | _ => match (a.get! i).isStrLit with
+        | _ => match (a.get! i).isStrLit? with
          | some fn => syntaxToExternEntries (i+1) (ExternEntry.standard backend fn :: entries)
          | none => Except.error "string literal expected"
    | _ => Except.error "identifier expected"
@ -63,10 +63,10 @@ match s with
 | Syntax.node _ args =>
  if args.size == 0 then Except.error "unexpected kind of argument"
  else
-    let (arity, i) : Option Nat × Nat := match (args.get! 0).isNatLit with
+    let (arity, i) : Option Nat × Nat := match (args.get! 0).isNatLit? with
      | some arity => (some arity, 1)
      | none       => (none, 0);
-    match (args.get! i).isStrLit with
+    match (args.get! i).isStrLit? with
    | some str =>
      if args.size == i+1 then
        Except.ok { arity := arity, entries := [ ExternEntry.standard `all str ] }
--- a/stage0/src/Init/Lean/Data/Name.lean
+++ b/stage0/src/Init/Lean/Data/Name.lean
@ -151,6 +151,11 @@ def appendIndexAfter : Name → Nat → Name
 | str p s _, idx => mkNameStr p (s ++ "_" ++ toString idx)
 | n,         idx => mkNameStr n ("_" ++ toString idx)

+def appendBefore : Name → String → Name
+| anonymous, pre => mkNameStr anonymous pre
+| str p s _, pre => mkNameStr p (pre ++ s)
+| num p n _, pre => mkNameNum (mkNameStr p pre) n
+
 /- The frontend does not allow user declarations to start with `_` in any of its parts.
   We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool
--- a/stage0/src/Init/Lean/Declaration.lean
+++ b/stage0/src/Init/Lean/Declaration.lean
@ -53,6 +53,8 @@ end ReducibilityHints
 structure ConstantVal :=
 (name : Name) (lparams : List Name) (type : Expr)

+instance ConstantVal.inhabited : Inhabited ConstantVal := ⟨{ name := arbitrary _, lparams := arbitrary _, type := arbitrary _ }⟩
+
 structure AxiomVal extends ConstantVal :=
 (isUnsafe : Bool)

@ -112,6 +114,9 @@ structure ConstructorVal extends ConstantVal :=
 (nfields : Nat)   -- Number of fields (i.e., arity - nparams)
 (isUnsafe : Bool)

+instance ConstructorVal.inhabited : Inhabited ConstructorVal :=
+⟨{ toConstantVal := arbitrary _, induct := arbitrary _, cidx := 0, nparams := 0, nfields := 0, isUnsafe := true }⟩
+
 /-- Information for reducing a recursor -/
 structure RecursorRule :=
 (ctor : Name)   -- Reduction rule for this Constructor
--- a/stage0/src/Init/Lean/Elab/Quotation.lean
+++ b/stage0/src/Init/Lean/Elab/Quotation.lean
@ -88,8 +88,8 @@ private partial def toPreterm (env : Environment) : Syntax → Except String Exp
    arg ← toPreterm $ args.get! 1;
    pure $ mkApp fn arg
  | `Lean.Parser.Term.paren => toPreterm $ (args.get! 1).getArg 0
-  | `strLit => pure $ mkStrLit $ stx.isStrLit.getD ""
-  | `numLit => pure $ mkNatLit $ stx.isNatLit.getD 0
+  | `strLit => pure $ mkStrLit $ stx.isStrLit?.getD ""
+  | `numLit => pure $ mkNatLit $ stx.isNatLit?.getD 0
  | k => panic! "stxQuot: unimplemented kind " ++ toString k

@[export lean_parse_stx_quot]
--- a/stage0/src/Init/Lean/Elab/Term.lean
+++ b/stage0/src/Init/Lean/Elab/Term.lean
@ -45,8 +45,18 @@ abbrev TermElab  := SyntaxNode → Option Expr → TermElabM Expr

 abbrev TermElabResult := EStateM.Result Exception State Expr

+instance TermElabM.inhabited {α} : Inhabited (TermElabM α) :=
+⟨throw $ Exception.other ""⟩
+
 instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩

+inductive Projection
+| num (fieldIdx  : Nat)
+| str (fieldName : String)
+
+instance Projection.hasToString : HasToString Projection :=
+⟨fun p => match p with | Projection.num n => toString n | Projection.str s => s⟩
+
 /--
  Execute `x`, save resulting expression and new state.
  If `x` fails, then it also stores exception and new state. -/
@ -141,6 +151,8 @@ def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.isDefEq t s
 def inferType (e : Expr) : TermElabM Expr := liftMetaM $ Meta.inferType e
 def whnf (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnf e
 def whnfForall (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfForall e
+def whnfCore (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfCore e
+def unfoldDefinition (e : Expr) : TermElabM (Option Expr) := liftMetaM $ Meta.unfoldDefinition e
 def instantiateMVars (e : Expr) : TermElabM Expr := liftMetaM $ Meta.instantiateMVars e
 def isClass (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass t
 def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar
@ -555,19 +567,34 @@ let argIdx    := 0;
 let instMVars := #[];
 elabAppArgsAux ref args expectedType? explicit argIdx namedArgs instMVars fType f

-private def elabAppProjs (ref : Syntax) (f : Expr) (projs : List String) (namedArgs : Array NamedArg) (args : Array Syntax)
-    (expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr :=
-- TODO
-elabAppArgs ref f namedArgs args expectedType? explicit
+private def elabAppProjsAux (ref : Syntax) (namedArgs : Array NamedArg) (args : Array Syntax) (expectedType? : Option Expr) (explicit : Bool)
+    : Expr → List Projection → TermElabM Expr
+| f, []          => elabAppArgs ref f namedArgs args expectedType? explicit
+| f, proj::projs => do
+  fType ← inferType f;
+  -- TODO
+  elabAppArgs ref f namedArgs args expectedType? explicit

-private partial def elabAppFn (ref : Syntax) : Syntax → Array NamedArg → Array Syntax → Option Expr → Bool → Array TermElabResult → TermElabM (Array TermElabResult)
-| f, namedArgs, args, expectedType?, explicit, acc =>
+private def elabAppProjs (ref : Syntax) (f : Expr) (projs : List Projection) (namedArgs : Array NamedArg) (args : Array Syntax)
+    (expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
+when (!projs.isEmpty && explicit) $ logErrorAndThrow ref "invalid use of projection notation with `@` modifier";
+elabAppProjsAux ref namedArgs args expectedType? explicit f projs
+
+private partial def elabAppFn (ref : Syntax) : Syntax → List Projection → Array NamedArg → Array Syntax → Option Expr → Bool → Array TermElabResult → TermElabM (Array TermElabResult)
+| f, projs, namedArgs, args, expectedType?, explicit, acc =>
  let k := f.getKind;
  if k == `Lean.Parser.Term.explicit then
    -- `f` is of the form `@ id`
-    elabAppFn (f.getArg 1) namedArgs args expectedType? true acc
+    elabAppFn (f.getArg 1) projs namedArgs args expectedType? true acc
  else if k == choiceKind then
-    f.getArgs.foldlM (fun acc f => elabAppFn f namedArgs args expectedType? explicit acc) acc
+    f.getArgs.foldlM (fun acc f => elabAppFn f projs namedArgs args expectedType? explicit acc) acc
+  else if k == `Lean.Parser.Term.proj then
+    -- term `.` (fieldIdx <|> ident)
+    let field := f.getArg 2;
+    match field.isFieldIdx?, field with
+    | some idx, _                      => elabAppFn (f.getArg 0) (Projection.num idx :: projs) namedArgs args expectedType? true acc
+    | _,        Syntax.ident _ val _ _ => elabAppFn (f.getArg 0) (Projection.str val.toString :: projs) namedArgs args expectedType? true acc
+    | _,        _                      => logErrorAndThrow field "unexpected kind of field access"
  else if k == `Lean.Parser.Term.id then
    -- ident (explicitUniv | namedPattern)?
    match f.getArg 0 with
@ -575,14 +602,15 @@ private partial def elabAppFn (ref : Syntax) : Syntax → Array NamedArg → Arr
      us     ← elabExplicitUniv (f.getArg 1); -- `namedPattern` should already have been expanded
      fprojs ← resolveName n preresolved us f;
      fprojs.foldlM
-        (fun acc ⟨f, projs⟩ => do
-          s ← observing $ elabAppProjs ref f projs namedArgs args expectedType? explicit;
+        (fun acc ⟨f, projs'⟩ => do
+          let projs' := projs'.map Projection.str;
+          s ← observing $ elabAppProjs ref f (projs' ++ projs) namedArgs args expectedType? explicit;
          pure $ acc.push s)
        acc
    | _ => unreachable!
  else do
    f ← withoutPostponing $ elabTerm f none;
-    s ← observing $ elabAppArgs ref f namedArgs args expectedType? explicit;
+    s ← observing $ elabAppProjs ref f projs namedArgs args expectedType? explicit;
    pure $ acc.push s

 private def getSuccess (candidates : Array TermElabResult) : Array TermElabResult :=
@ -624,7 +652,7 @@ private def elabAppAux (ref : Syntax) (f : Syntax) (namedArgs : Array NamedArg)
   Another (more expensive) option is: execute, and if successes > 1, `mayPostpone == true`, and `expectedType? == some ?m` where `?m` is not assigned,
   then we postpone `elabAppAux`. It is more expensive because we would have to re-elaborate the whole thing after we assign `?m`.
   We **can't** continue from `TermElabResult` since they contain a snapshot of the state, and state has changed. -/
-candidates ← elabAppFn ref f namedArgs args expectedType? false #[];
+candidates ← elabAppFn ref f [] namedArgs args expectedType? false #[];
 if candidates.size == 1 then
  applyResult $ candidates.get! 0
 else
@ -671,6 +699,7 @@ fun stx expectedType? => do
@[builtinTermElab «id»] def elabId : TermElab := elabApp
@[builtinTermElab explicit] def elabExplicit : TermElab := elabApp
@[builtinTermElab choice] def elabChoice : TermElab := elabApp
+@[builtinTermElab proj] def elabProj : TermElab := elabApp

 end Term

--- a/stage0/src/Init/Lean/Meta/Basic.lean
+++ b/stage0/src/Init/Lean/Meta/Basic.lean
@ -508,19 +508,22 @@ resettingSynthInstanceCache $
    (reducing?        : Bool) (maxFVars? : Option Nat)
    (k                : Array Expr → Expr → MetaM α)
    : LocalContext → Array Expr → Nat → Expr → MetaM α
-| lctx, fvars, j, Expr.forallE n d b c => do
-  let d     := d.instantiateRevRange j fvars.size fvars;
-  fvarId ← mkFreshId;
-  let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo;
-  let fvar  := mkFVar fvarId;
-  let fvars := fvars.push fvar;
+| lctx, fvars, j, type@(Expr.forallE n d b c) => do
+  let process : Unit → MetaM α := fun _ => do {
+    let d     := d.instantiateRevRange j fvars.size fvars;
+    fvarId ← mkFreshId;
+    let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo;
+    let fvar  := mkFVar fvarId;
+    let fvars := fvars.push fvar;
+    forallTelescopeReducingAuxAux lctx fvars j b
+  };
  match maxFVars? with
-  | none          => forallTelescopeReducingAuxAux lctx fvars j b
+  | none          => process ()
  | some maxFVars =>
    if fvars.size < maxFVars then
-      forallTelescopeReducingAuxAux lctx fvars j b
+      process ()
    else
-      let type := b.instantiateRevRange j fvars.size fvars;
+      let type := type.instantiateRevRange j fvars.size fvars;
      adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
        withNewLocalInstances isClassExpensive fvars j $
          k fvars type
@ -616,18 +619,21 @@ lambdaTelescopeAux k lctx #[] 0 e
 private partial def forallMetaTelescopeReducingAux
    (reducing? : Bool) (maxMVars? : Option Nat)
    : Array Expr → Array BinderInfo → Nat → Expr → MetaM (Array Expr × Array BinderInfo × Expr)
-| mvars, bis, j, Expr.forallE n d b c => do
-  let d     := d.instantiateRevRange j mvars.size mvars;
-  mvar ← mkFreshExprMVar d;
-  let mvars := mvars.push mvar;
-  let bis   := bis.push c.binderInfo;
+| mvars, bis, j, type@(Expr.forallE n d b c) => do
+  let process : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do {
+    let d     := d.instantiateRevRange j mvars.size mvars;
+    mvar ← mkFreshExprMVar d;
+    let mvars := mvars.push mvar;
+    let bis   := bis.push c.binderInfo;
+    forallMetaTelescopeReducingAux mvars bis j b
+  };
  match maxMVars? with
-  | none          => forallMetaTelescopeReducingAux mvars bis j b
+  | none          => process ()
  | some maxMVars =>
    if mvars.size < maxMVars then
-      forallMetaTelescopeReducingAux mvars bis j b
+      process ()
    else
-      let type := b.instantiateRevRange j mvars.size mvars;
+      let type := type.instantiateRevRange j mvars.size mvars;
      pure (mvars, bis, type)
 | mvars, bis, j, type =>
  let type := type.instantiateRevRange j mvars.size mvars;
@ -651,22 +657,28 @@ forallMetaTelescopeReducingAux true maxMVars? #[] #[] 0 e
 /-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions. -/
 private partial def lambdaMetaTelescopeAux (maxMVars? : Option Nat)
    : Array Expr → Array BinderInfo → Nat → Expr → MetaM (Array Expr × Array BinderInfo × Expr)
-| mvars, bis, j, Expr.lam n d b c => do
-  let d     := d.instantiateRevRange j mvars.size mvars;
-  mvar ← mkFreshExprMVar d;
-  let mvars := mvars.push mvar;
-  let bis   := bis.push c.binderInfo;
+| mvars, bis, j, type => do
+  let finalize : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do {
+    let type := type.instantiateRevRange j mvars.size mvars;
+    pure (mvars, bis, type)
+  };
+  let process : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do {
+    match type with
+    | Expr.lam n d b c => do
+      let d     := d.instantiateRevRange j mvars.size mvars;
+      mvar ← mkFreshExprMVar d;
+      let mvars := mvars.push mvar;
+      let bis   := bis.push c.binderInfo;
+      lambdaMetaTelescopeAux mvars bis j b
+    | _ => finalize ()
+  };
  match maxMVars? with
-  | none          => lambdaMetaTelescopeAux mvars bis j b
+  | none          => process ()
  | some maxMVars =>
    if mvars.size < maxMVars then
-      lambdaMetaTelescopeAux mvars bis j b
+      process ()
    else
-      let type := b.instantiateRevRange j mvars.size mvars;
-      pure (mvars, bis, type)
-| mvars, bis, j, type =>
-  let type := type.instantiateRevRange j mvars.size mvars;
-  pure (mvars, bis, type)
+      finalize ()

 /-- Similar to `forallMetaTelescope` but for lambda expressions. -/
 def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
--- a/stage0/src/Init/Lean/Meta/DiscrTree.lean
+++ b/stage0/src/Init/Lean/Meta/DiscrTree.lean
@ -252,9 +252,28 @@ match e.getAppFn with
 | Expr.fvar fvarId _ => let nargs := e.getAppNumArgs; pure (Key.fvar fvarId nargs, e.getAppRevArgs)
 | Expr.mvar mvarId _ =>
  if isMatch? then pure (Key.other, #[])
-  else condM (isReadOnlyOrSyntheticExprMVar mvarId)
-    (pure (Key.other, #[]))
-    (pure (Key.star, #[]))
+  else do
+    ctx ← read;
+    if ctx.config.isDefEqStuckEx then
+      /-
+        When the configuration flag `isDefEqStuckEx` is set to true,
+        we want `isDefEq` to throw an exception whenever it tries to assign
+        a read-only metavariable.
+        This feature is useful for type class resolution where
+        we may want to notify the caller that the TC problem may be solveable
+        later after it assigns `?m`.
+        The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`.
+        That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (HasAdd ?m)`
+        where `?m` is a read-only metavariable, and the discrimination tree contains the keys
+        `HadAdd Nat` and `HasAdd Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as
+        a regular metavariable here, otherwise we return the empty set of candidates.
+        This is incorrect because it is equivalent to saying that there is no solution even if
+        the caller assigns `?m` and try again. -/
+      pure (Key.star, #[])
+    else
+      condM (isReadOnlyOrSyntheticExprMVar mvarId)
+        (pure (Key.other, #[]))
+        (pure (Key.star, #[]))
 | _                  => pure (Key.other, #[])

 private abbrev getMatchKeyArgs (e : Expr) : MetaM (Key × Array Expr) :=
--- a/stage0/src/Init/Lean/Structure.lean
+++ b/stage0/src/Init/Lean/Structure.lean
@ -0,0 +1,124 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Helper functions for retrieving structure information.
+-/
+prelude
+import Init.Lean.Environment
+import Init.Lean.ProjFns
+
+namespace Lean
+
+/--
+  Return true iff `constName` is the a non-recursive inductive
+  datatype that has only one constructor. -/
+def isStructureLike (env : Environment) (constName : Name) : Bool :=
+match env.find constName with
+| some (ConstantInfo.inductInfo { isRec := false, ctors := [ctor], .. }) => true
+| _ => false
+
+/-- We mark subobject fields by prefixing them with "_" in the structure's intro rule. -/
+def mkInternalSubobjectFieldName (fieldName : Name) : Name :=
+fieldName.appendBefore "_"
+
+def isInternalSubobjectFieldName : Name → Bool
+| Name.str _ s _ => s.length > 0 && s.get 0 == '_'
+| _              => false
+
+def deinternalizeFieldName : Name → Name
+| n@(Name.str p s _) => if s.length > 0 && s.get 0 == '_' then mkNameStr p (s.drop 1) else n
+| n                  => n
+
+def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal :=
+match env.find constName with
+| some (ConstantInfo.inductInfo { nparams := nparams, isRec := false, ctors := [ctorName], .. }) =>
+  match env.find ctorName with
+  | some (ConstantInfo.ctorInfo val) => val
+  | _ => panic! "ill-formed environment"
+| _ => panic! "structure expected"
+
+private def getStructureFieldsAux (nparams : Nat) : Nat → Expr → Array Name → Array Name
+| i, Expr.forallE n d b _, fieldNames =>
+  if i < nparams then
+    getStructureFieldsAux (i+1) b fieldNames
+  else
+    getStructureFieldsAux (i+1) b (fieldNames.push $ deinternalizeFieldName n)
+| _, _, fieldNames => fieldNames
+
+def getStructureFields (env : Environment) (structName : Name) : Array Name :=
+let ctor := getStructureCtor env structName;
+getStructureFieldsAux ctor.nparams 0 ctor.type #[]
+
+private def isSubobjectFieldAux (nparams : Nat) (target : Name) : Nat → Expr → Option Name
+| i, Expr.forallE n d b _ =>
+  if i < nparams then
+    isSubobjectFieldAux (i+1) b
+  else if n == target then
+    match d.getAppFn with
+    | Expr.const parentStructName _ _ => some parentStructName
+    | _ => panic! "ill-formed structure"
+  else
+    isSubobjectFieldAux (i+1) b
+| _, _ => none
+
+/-- If `fieldName` represents the relation to a parent structure `S`, return `S` -/
+def isSubobjectField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name :=
+let ctor := getStructureCtor env structName;
+isSubobjectFieldAux ctor.nparams (mkInternalSubobjectFieldName fieldName) 0 ctor.type
+
+/-- Return immediate parent structures -/
+def getParentStructures (env : Environment) (structName : Name) : Array Name :=
+let fieldNames := getStructureFields env structName;
+fieldNames.foldl
+  (fun (acc : Array Name) fieldName =>
+    match isSubobjectField? env structName fieldName with
+    | some parentStructName => acc.push parentStructName
+    | none                  => acc)
+  #[]
+
+/-- `findField? env S fname`. If `fname` is defined in a parent `S'` of `S`, return `S'` -/
+partial def findField? (env : Environment) : Name → Name → Option Name
+| structName, fieldName =>
+  if (getStructureFields env structName).contains fieldName then
+    some structName
+  else
+    (getParentStructures env structName).find? $ fun parentStructName => findField? parentStructName fieldName
+
+private partial def getStructureFieldsFlattenedAux (env : Environment) : Name → Array Name → Array Name
+| structName, fullNames =>
+  (getStructureFields env structName).foldl
+    (fun (fullNames : Array Name) (fieldName : Name) =>
+      let fullNames := fullNames.push fieldName;
+      match isSubobjectField? env structName fieldName with
+      | some parentStructName => getStructureFieldsFlattenedAux parentStructName fullNames
+      | none                  => fullNames)
+    fullNames
+
+def getStructureFieldsFlattened (env : Environment) (structName : Name) : Array Name :=
+getStructureFieldsFlattenedAux env structName #[]
+
+private def hasProjFn (env : Environment) (structName : Name) (nparams : Nat) : Nat → Expr → Bool
+| i, Expr.forallE n d b _ =>
+  if i < nparams then
+    hasProjFn (i+1) b
+  else
+    let fullFieldName := structName ++ deinternalizeFieldName n;
+    env.isProjectionFn fullFieldName
+| _, _ => false
+
+/--
+  Return true if `constName` is the name of an inductive datatype
+  created using the `structure` or `class` commands.
+
+  We perform the check by testing whether auxiliary projection functions
+  have been created. -/
+def isStructure (env : Environment) (constName : Name) : Bool :=
+if isStructureLike env constName then
+  let ctor := getStructureCtor env constName;
+  hasProjFn env constName ctor.nparams 0 ctor.type
+else
+  false
+
+end Lean
--- a/stage0/src/Init/Lean/Syntax.lean
+++ b/stage0/src/Init/Lean/Syntax.lean
@ -364,7 +364,7 @@ mkStxNumLit (toString val)

 namespace Syntax

-def isStrLit : Syntax → Option String
+def isStrLit? : Syntax → Option String
 | Syntax.node k args   =>
  if k == strLitKind && args.size == 1 then
    match args.get! 0 with
@ -443,19 +443,19 @@ def isNatLitAux (nodeKind : SyntaxNodeKind) : Syntax → Option Nat
    none
 | _ => none

-def isNatLit (s : Syntax) : Option Nat :=
+def isNatLit? (s : Syntax) : Option Nat :=
 isNatLitAux numLitKind s

-def isFieldIdx (s : Syntax) : Option Nat :=
+def isFieldIdx? (s : Syntax) : Option Nat :=
 isNatLitAux fieldIdxKind s

-def isIdOrAtom : Syntax → Option String
+def isIdOrAtom? : Syntax → Option String
 | Syntax.atom _ val           => some val
 | Syntax.ident _ rawVal _ _   => some rawVal.toString
 | _ => none

 def toNat (stx : Syntax) : Nat :=
-match stx.isNatLit with
+match stx.isNatLit? with
 | some val => val
 | none     => 0

--- a/stage0/src/frontends/lean/structure_cmd.cpp
+++ b/stage0/src/frontends/lean/structure_cmd.cpp
@ -136,20 +136,6 @@ buffer<name> get_parent_structures(environment const & env, name const & S_name)
    return parents;
 }

-name_set get_ancestor_structures(environment const & env, name const & S_name) {
-    name_set ns;
-    std::function<void(name const &)> go = [&](name const & n) {
-        for (auto const & p : get_parent_structures(env, n)) {
-            if (!ns.contains(p)) {
-                ns.insert(p);
-                go(p);
-            }
-        }
-    };
-    go(S_name);
-    return ns;
-}
-
 optional<name> find_field(environment const & env, name const & S_name, name const & fname) {
    for (auto const & n : get_structure_fields(env, S_name))
        if (n == fname)
--- a/stage0/src/library/constructions/projection.cpp
+++ b/stage0/src/library/constructions/projection.cpp
@ -71,7 +71,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
    }
    expr C_A                     = mk_app(mk_constant(n, lvls), params);
    binder_info c_bi             = inst_implicit ? mk_inst_implicit_binder_info() : mk_binder_info();
-    expr c                       = lctx.mk_local_decl(ngen, name("c"), C_A, c_bi);
+    expr c                       = lctx.mk_local_decl(ngen, name("self"), C_A, c_bi);
    buffer<expr> cnstr_type_args; // arguments that are not parameters
    expr it = cnstr_type;
    while (is_pi(it)) {
--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
--- a/stage0/stdlib/Init/Lean.c
+++ b/stage0/stdlib/Init/Lean.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean
-// Imports: Init.Lean.Compiler Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser Init.Lean.ReducibilityAttrs Init.Lean.Elab Init.Lean.EqnCompiler Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.AuxRecursor Init.Lean.Linter Init.Lean.Meta Init.Lean.Eval
+// Imports: Init.Lean.Compiler Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser Init.Lean.ReducibilityAttrs Init.Lean.Elab Init.Lean.EqnCompiler Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.AuxRecursor Init.Lean.Linter Init.Lean.Meta Init.Lean.Eval Init.Lean.Structure
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -30,6 +30,7 @@ lean_object* initialize_Init_Lean_AuxRecursor(lean_object*);
 lean_object* initialize_Init_Lean_Linter(lean_object*);
 lean_object* initialize_Init_Lean_Meta(lean_object*);
 lean_object* initialize_Init_Lean_Eval(lean_object*);
+lean_object* initialize_Init_Lean_Structure(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean(lean_object* w) {
 lean_object * res;
@ -86,6 +87,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Eval(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Structure(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Init/Lean/Compiler/ExternAttr.c
+++ b/stage0/stdlib/Init/Lean/Compiler/ExternAttr.c
@ -77,6 +77,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkExternAttr___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_expandExternPatternAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
 lean_object* l_Lean_expandExternPatternAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData___closed__5;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
@ -85,7 +86,6 @@ lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData
 lean_object* l_Lean_expandExternPatternAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkExternAttr___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkExternAttr___closed__2;
-lean_object* l_Lean_Syntax_isStrLit(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Array_qsortAux___main___at_Lean_mkExternAttr___spec__3___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_List_reprAux___main___rarg___closed__1;
@ -106,6 +106,7 @@ lean_object* l_List_foldl___main___at_Lean_mkSimpleFnCall___spec__1___boxed(lean
 uint8_t l_String_Iterator_hasNext(lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_isExternC___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_isIdOrAtom_x3f(lean_object*);
 extern lean_object* l_Option_HasRepr___rarg___closed__3;
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData(lean_object*);
 lean_object* lean_get_extern_attr_data(lean_object*, lean_object*);
@ -133,7 +134,6 @@ lean_object* l_Lean_expandExternPatternAux(lean_object*, lean_object*, lean_obje
 lean_object* l_Lean_getExternEntryForAux___boxed(lean_object*, lean_object*);
 lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkExternAttr___closed__4;
-lean_object* l_Lean_Syntax_isIdOrAtom(lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* lean_io_initializing(lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
@ -286,11 +286,11 @@ if (x_11 == 0)
 {
 lean_object* x_12; lean_object* x_13; 
 x_12 = lean_array_get(x_6, x_1, x_10);
-x_13 = l_Lean_Syntax_isIdOrAtom(x_12);
+x_13 = l_Lean_Syntax_isIdOrAtom_x3f(x_12);
 if (lean_obj_tag(x_13) == 0)
 {
 lean_object* x_14; 
-x_14 = l_Lean_Syntax_isStrLit(x_12);
+x_14 = l_Lean_Syntax_isStrLit_x3f(x_12);
 lean_dec(x_12);
 if (lean_obj_tag(x_14) == 0)
 {
@ -337,7 +337,7 @@ lean_dec(x_21);
 if (x_25 == 0)
 {
 lean_object* x_26; 
-x_26 = l_Lean_Syntax_isStrLit(x_12);
+x_26 = l_Lean_Syntax_isStrLit_x3f(x_12);
 lean_dec(x_12);
 if (lean_obj_tag(x_26) == 0)
 {
@ -374,7 +374,7 @@ lean_dec(x_12);
 x_33 = lean_nat_add(x_10, x_9);
 lean_dec(x_10);
 x_34 = lean_array_get(x_6, x_1, x_33);
-x_35 = l_Lean_Syntax_isStrLit(x_34);
+x_35 = l_Lean_Syntax_isStrLit_x3f(x_34);
 lean_dec(x_34);
 if (lean_obj_tag(x_35) == 0)
 {
@ -633,7 +633,7 @@ lean_inc(x_9);
 lean_dec(x_7);
 x_10 = l_Lean_stxInh;
 x_11 = lean_array_get(x_10, x_3, x_9);
-x_12 = l_Lean_Syntax_isStrLit(x_11);
+x_12 = l_Lean_Syntax_isStrLit_x3f(x_11);
 lean_dec(x_11);
 if (lean_obj_tag(x_12) == 0)
 {
--- a/stage0/stdlib/Init/Lean/Data/Name.c
+++ b/stage0/stdlib/Init/Lean/Data/Name.c
@ -125,6 +125,7 @@ size_t lean_usize_mix_hash(size_t, size_t);
 uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
 lean_object* l_Lean_Name_isPrefixOf___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_NameSet_insert(lean_object*, lean_object*);
+lean_object* l_Lean_Name_appendBefore(lean_object*, lean_object*);
 lean_object* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__3(lean_object*);
 lean_object* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_NameMap_contains___spec__1___rarg(lean_object*, lean_object*);
@ -1299,6 +1300,44 @@ return x_7;
 }
 }
 }
+lean_object* l_Lean_Name_appendBefore(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+switch (lean_obj_tag(x_1)) {
+case 0:
+{
+lean_object* x_3; 
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+case 1:
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+x_5 = lean_ctor_get(x_1, 1);
+lean_inc(x_5);
+lean_dec(x_1);
+x_6 = lean_string_append(x_2, x_5);
+lean_dec(x_5);
+x_7 = lean_name_mk_string(x_4, x_6);
+return x_7;
+}
+default: 
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = lean_ctor_get(x_1, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_1, 1);
+lean_inc(x_9);
+lean_dec(x_1);
+x_10 = lean_name_mk_string(x_8, x_2);
+x_11 = lean_name_mk_numeral(x_10, x_9);
+return x_11;
+}
+}
+}
+}
 uint8_t l_Lean_Name_isInternal___main(lean_object* x_1) {
 _start:
 {
--- a/stage0/stdlib/Init/Lean/Declaration.c
+++ b/stage0/stdlib/Init/Lean/Declaration.c
@ -14,8 +14,10 @@
 extern "C" {
 #endif
 lean_object* l_Lean_ReducibilityHints_lt___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_ConstantVal_inhabited___closed__1;
 lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ConstantInfo_instantiateValueLevelParams___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_ConstantVal_inhabited___closed__2;
 lean_object* l_Lean_ConstantInfo_value_x3f___boxed(lean_object*);
 lean_object* l_Lean_RecursorVal_getMajorIdx___boxed(lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
@ -25,12 +27,14 @@ lean_object* l_Lean_ConstantInfo_value_x21___boxed(lean_object*);
 lean_object* l_Lean_ConstantInfo_value_x21___closed__2;
 lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*);
 lean_object* l_Lean_ConstantInfo_instantiateTypeLevelParams___boxed(lean_object*, lean_object*);
+extern lean_object* l_Lean_Expr_Inhabited___closed__1;
 uint8_t l_UInt32_decLt(uint32_t, uint32_t);
 lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_ConstantInfo_toConstantVal(lean_object*);
 lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
 lean_object* l_Lean_ConstantInfo_hasValue___boxed(lean_object*);
 lean_object* l_Lean_ConstantInfo_name(lean_object*);
+lean_object* l_Lean_ConstantVal_inhabited;
 lean_object* l_Lean_ConstantInfo_toConstantVal___boxed(lean_object*);
 uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
 lean_object* l_Lean_RecursorVal_getInduct___boxed(lean_object*);
@ -39,6 +43,7 @@ lean_object* l_Lean_ConstantInfo_isCtor___boxed(lean_object*);
 lean_object* l_Lean_ConstantInfo_hints(lean_object*);
 lean_object* l_Lean_ConstantInfo_type(lean_object*);
 lean_object* l_Lean_ConstantInfo_value_x3f(lean_object*);
+lean_object* l_Lean_ConstructorVal_inhabited___closed__1;
 lean_object* l_Lean_RecursorVal_getInduct(lean_object*);
 lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
 lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
@ -47,6 +52,7 @@ lean_object* l_panic(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_InductiveVal_nctors___boxed(lean_object*);
 lean_object* l_Lean_Name_getPrefix(lean_object*);
 lean_object* l_Lean_ConstantInfo_name___boxed(lean_object*);
+lean_object* l_Lean_ConstructorVal_inhabited;
 extern lean_object* l_Lean_Expr_Inhabited;
 lean_object* l_Lean_InductiveVal_nctors(lean_object*);
 lean_object* l_Lean_ConstantInfo_value_x21___closed__3;
@ -127,6 +133,40 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
+lean_object* _init_l_Lean_ConstantVal_inhabited___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = lean_box(0);
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_ConstantVal_inhabited___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = lean_box(0);
+x_2 = l_Lean_ConstantVal_inhabited___closed__1;
+x_3 = l_Lean_Expr_Inhabited___closed__1;
+x_4 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_ConstantVal_inhabited() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_ConstantVal_inhabited___closed__2;
+return x_1;
+}
+}
 lean_object* l_Lean_InductiveVal_nctors(lean_object* x_1) {
 _start:
 {
@ -146,6 +186,32 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* _init_l_Lean_ConstructorVal_inhabited___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; 
+x_1 = l_Lean_ConstantVal_inhabited___closed__2;
+x_2 = lean_box(0);
+x_3 = lean_unsigned_to_nat(0u);
+x_4 = 1;
+x_5 = lean_alloc_ctor(0, 5, 1);
+lean_ctor_set(x_5, 0, x_1);
+lean_ctor_set(x_5, 1, x_2);
+lean_ctor_set(x_5, 2, x_3);
+lean_ctor_set(x_5, 3, x_3);
+lean_ctor_set(x_5, 4, x_3);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5, x_4);
+return x_5;
+}
+}
+lean_object* _init_l_Lean_ConstructorVal_inhabited() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_ConstructorVal_inhabited___closed__1;
+return x_1;
+}
+}
 lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object* x_1) {
 _start:
 {
@ -367,7 +433,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_ConstantInfo_value_x21___closed__1;
-x_2 = lean_unsigned_to_nat(194u);
+x_2 = lean_unsigned_to_nat(199u);
 x_3 = lean_unsigned_to_nat(31u);
 x_4 = l_Lean_ConstantInfo_value_x21___closed__2;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -496,6 +562,16 @@ if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Lean_ReducibilityHints_Inhabited = _init_l_Lean_ReducibilityHints_Inhabited();
 lean_mark_persistent(l_Lean_ReducibilityHints_Inhabited);
+l_Lean_ConstantVal_inhabited___closed__1 = _init_l_Lean_ConstantVal_inhabited___closed__1();
+lean_mark_persistent(l_Lean_ConstantVal_inhabited___closed__1);
+l_Lean_ConstantVal_inhabited___closed__2 = _init_l_Lean_ConstantVal_inhabited___closed__2();
+lean_mark_persistent(l_Lean_ConstantVal_inhabited___closed__2);
+l_Lean_ConstantVal_inhabited = _init_l_Lean_ConstantVal_inhabited();
+lean_mark_persistent(l_Lean_ConstantVal_inhabited);
+l_Lean_ConstructorVal_inhabited___closed__1 = _init_l_Lean_ConstructorVal_inhabited___closed__1();
+lean_mark_persistent(l_Lean_ConstructorVal_inhabited___closed__1);
+l_Lean_ConstructorVal_inhabited = _init_l_Lean_ConstructorVal_inhabited();
+lean_mark_persistent(l_Lean_ConstructorVal_inhabited);
 l_Lean_ConstantInfo_value_x21___closed__1 = _init_l_Lean_ConstantInfo_value_x21___closed__1();
 lean_mark_persistent(l_Lean_ConstantInfo_value_x21___closed__1);
 l_Lean_ConstantInfo_value_x21___closed__2 = _init_l_Lean_ConstantInfo_value_x21___closed__2();
--- a/stage0/stdlib/Init/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/Quotation.c
@ -77,6 +77,7 @@ extern lean_object* l_Lean_Parser_Term_id___elambda__1___closed__2;
 extern lean_object* l_Lean_numLitKind;
 extern lean_object* l_Lean_strLitKind;
 lean_object* l___private_Init_Lean_Elab_Quotation_7__quote(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
 extern lean_object* l_Lean_Parser_Term_antiquot___elambda__1___rarg___closed__1;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_numLitKind___closed__1;
@ -92,7 +93,6 @@ extern lean_object* l_Lean_Parser_Term_id___elambda__1___closed__1;
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_7__quote___main___spec__8___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_1__const(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_8__toPreterm___main___closed__2;
-lean_object* l_Lean_Syntax_isStrLit(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_8__toPreterm___main___closed__1;
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_7__quote___main___spec__3___boxed(lean_object*, lean_object*, lean_object*);
@ -2706,7 +2706,7 @@ else
 lean_object* x_30; 
 lean_dec(x_18);
 lean_dec(x_4);
-x_30 = l_Lean_Syntax_isStrLit(x_2);
+x_30 = l_Lean_Syntax_isStrLit_x3f(x_2);
 lean_dec(x_2);
 if (lean_obj_tag(x_30) == 0)
 {
--- a/stage0/stdlib/Init/Lean/Elab/Term.c
+++ b/stage0/stdlib/Init/Lean/Elab/Term.c
--- a/stage0/stdlib/Init/Lean/Meta/Basic.c
+++ b/stage0/stdlib/Init/Lean/Meta/Basic.c
--- a/stage0/stdlib/Init/Lean/Meta/DiscrTree.c
+++ b/stage0/stdlib/Init/Lean/Meta/DiscrTree.c
@ -5253,372 +5253,408 @@ case 2:
 lean_dec(x_7);
 if (x_2 == 0)
 {
-lean_object* x_17; lean_object* x_18; 
-lean_free_object(x_5);
-x_17 = lean_ctor_get(x_9, 0);
+lean_object* x_17; uint8_t x_18; 
+x_17 = lean_ctor_get(x_3, 0);
 lean_inc(x_17);
-lean_dec(x_9);
-x_18 = l_Lean_Meta_isReadOnlyOrSyntheticExprMVar(x_17, x_3, x_8);
-lean_dec(x_3);
-if (lean_obj_tag(x_18) == 0)
+x_18 = lean_ctor_get_uint8(x_17, sizeof(void*)*1 + 3);
+lean_dec(x_17);
+if (x_18 == 0)
 {
-lean_object* x_19; uint8_t x_20; 
-x_19 = lean_ctor_get(x_18, 0);
+lean_object* x_19; lean_object* x_20; 
+lean_free_object(x_5);
+x_19 = lean_ctor_get(x_9, 0);
 lean_inc(x_19);
-x_20 = lean_unbox(x_19);
-lean_dec(x_19);
-if (x_20 == 0)
+lean_dec(x_9);
+x_20 = l_Lean_Meta_isReadOnlyOrSyntheticExprMVar(x_19, x_3, x_8);
+lean_dec(x_3);
+if (lean_obj_tag(x_20) == 0)
 {
-uint8_t x_21; 
-x_21 = !lean_is_exclusive(x_18);
-if (x_21 == 0)
+lean_object* x_21; uint8_t x_22; 
+x_21 = lean_ctor_get(x_20, 0);
+lean_inc(x_21);
+x_22 = lean_unbox(x_21);
+lean_dec(x_21);
+if (x_22 == 0)
 {
-lean_object* x_22; lean_object* x_23; 
-x_22 = lean_ctor_get(x_18, 0);
-lean_dec(x_22);
-x_23 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__2;
-lean_ctor_set(x_18, 0, x_23);
-return x_18;
-}
-else
+uint8_t x_23; 
+x_23 = !lean_is_exclusive(x_20);
+if (x_23 == 0)
 {
-lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-x_24 = lean_ctor_get(x_18, 1);
-lean_inc(x_24);
-lean_dec(x_18);
+lean_object* x_24; lean_object* x_25; 
+x_24 = lean_ctor_get(x_20, 0);
+lean_dec(x_24);
 x_25 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__2;
-x_26 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_26, 0, x_25);
-lean_ctor_set(x_26, 1, x_24);
-return x_26;
+lean_ctor_set(x_20, 0, x_25);
+return x_20;
+}
+else
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = lean_ctor_get(x_20, 1);
+lean_inc(x_26);
+lean_dec(x_20);
+x_27 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__2;
+x_28 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_28, 0, x_27);
+lean_ctor_set(x_28, 1, x_26);
+return x_28;
 }
 }
 else
 {
-uint8_t x_27; 
-x_27 = !lean_is_exclusive(x_18);
-if (x_27 == 0)
+uint8_t x_29; 
+x_29 = !lean_is_exclusive(x_20);
+if (x_29 == 0)
 {
-lean_object* x_28; lean_object* x_29; 
-x_28 = lean_ctor_get(x_18, 0);
-lean_dec(x_28);
-x_29 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
-lean_ctor_set(x_18, 0, x_29);
-return x_18;
-}
-else
-{
-lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_18, 1);
-lean_inc(x_30);
-lean_dec(x_18);
+lean_object* x_30; lean_object* x_31; 
+x_30 = lean_ctor_get(x_20, 0);
+lean_dec(x_30);
 x_31 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
-x_32 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_32, 0, x_31);
-lean_ctor_set(x_32, 1, x_30);
-return x_32;
+lean_ctor_set(x_20, 0, x_31);
+return x_20;
+}
+else
+{
+lean_object* x_32; lean_object* x_33; lean_object* x_34; 
+x_32 = lean_ctor_get(x_20, 1);
+lean_inc(x_32);
+lean_dec(x_20);
+x_33 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
+x_34 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_34, 0, x_33);
+lean_ctor_set(x_34, 1, x_32);
+return x_34;
 }
 }
 }
 else
 {
-uint8_t x_33; 
-x_33 = !lean_is_exclusive(x_18);
-if (x_33 == 0)
+uint8_t x_35; 
+x_35 = !lean_is_exclusive(x_20);
+if (x_35 == 0)
 {
-return x_18;
+return x_20;
 }
 else
 {
-lean_object* x_34; lean_object* x_35; lean_object* x_36; 
-x_34 = lean_ctor_get(x_18, 0);
-x_35 = lean_ctor_get(x_18, 1);
-lean_inc(x_35);
-lean_inc(x_34);
-lean_dec(x_18);
-x_36 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_36, 0, x_34);
-lean_ctor_set(x_36, 1, x_35);
-return x_36;
+lean_object* x_36; lean_object* x_37; lean_object* x_38; 
+x_36 = lean_ctor_get(x_20, 0);
+x_37 = lean_ctor_get(x_20, 1);
+lean_inc(x_37);
+lean_inc(x_36);
+lean_dec(x_20);
+x_38 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_38, 0, x_36);
+lean_ctor_set(x_38, 1, x_37);
+return x_38;
 }
 }
 }
 else
 {
-lean_object* x_37; 
+lean_object* x_39; 
 lean_dec(x_9);
 lean_dec(x_3);
-x_37 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
-lean_ctor_set(x_5, 0, x_37);
+x_39 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__2;
+lean_ctor_set(x_5, 0, x_39);
+return x_5;
+}
+}
+else
+{
+lean_object* x_40; 
+lean_dec(x_9);
+lean_dec(x_3);
+x_40 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
+lean_ctor_set(x_5, 0, x_40);
 return x_5;
 }
 }
 case 4:
 {
-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_object* x_44; 
+lean_object* x_41; 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_dec(x_3);
-x_38 = lean_ctor_get(x_9, 0);
-lean_inc(x_38);
+x_41 = lean_ctor_get(x_9, 0);
+lean_inc(x_41);
 lean_dec(x_9);
-x_39 = lean_unsigned_to_nat(0u);
-x_40 = l_Lean_Expr_getAppNumArgsAux___main(x_7, x_39);
-lean_inc(x_40);
-x_41 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_41, 0, x_38);
-lean_ctor_set(x_41, 1, x_40);
-x_42 = lean_mk_empty_array_with_capacity(x_40);
-lean_dec(x_40);
-x_43 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_7, x_42);
+x_42 = lean_unsigned_to_nat(0u);
+x_43 = l_Lean_Expr_getAppNumArgsAux___main(x_7, x_42);
+lean_inc(x_43);
 x_44 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_44, 0, x_41);
 lean_ctor_set(x_44, 1, x_43);
-lean_ctor_set(x_5, 0, x_44);
+x_45 = lean_mk_empty_array_with_capacity(x_43);
+lean_dec(x_43);
+x_46 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_7, x_45);
+x_47 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_47, 0, x_44);
+lean_ctor_set(x_47, 1, x_46);
+lean_ctor_set(x_5, 0, x_47);
 return x_5;
 }
 case 9:
 {
-lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; 
+lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; 
 lean_dec(x_7);
 lean_dec(x_3);
-x_45 = lean_ctor_get(x_9, 0);
-lean_inc(x_45);
+x_48 = lean_ctor_get(x_9, 0);
+lean_inc(x_48);
 lean_dec(x_9);
-x_46 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_46, 0, x_45);
-x_47 = l_Array_empty___closed__1;
-x_48 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_48, 0, x_46);
-lean_ctor_set(x_48, 1, x_47);
-lean_ctor_set(x_5, 0, x_48);
+x_49 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_49, 0, x_48);
+x_50 = l_Array_empty___closed__1;
+x_51 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_51, 0, x_49);
+lean_ctor_set(x_51, 1, x_50);
+lean_ctor_set(x_5, 0, x_51);
 return x_5;
 }
 default: 
 {
-lean_object* x_49; 
+lean_object* x_52; 
 lean_dec(x_9);
 lean_dec(x_7);
 lean_dec(x_3);
-x_49 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
-lean_ctor_set(x_5, 0, x_49);
+x_52 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
+lean_ctor_set(x_5, 0, x_52);
 return x_5;
 }
 }
 }
 else
 {
-lean_object* x_50; lean_object* x_51; lean_object* x_52; 
-x_50 = lean_ctor_get(x_5, 0);
-x_51 = lean_ctor_get(x_5, 1);
-lean_inc(x_51);
-lean_inc(x_50);
+lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_53 = lean_ctor_get(x_5, 0);
+x_54 = lean_ctor_get(x_5, 1);
+lean_inc(x_54);
+lean_inc(x_53);
 lean_dec(x_5);
-x_52 = l_Lean_Expr_getAppFn___main(x_50);
-switch (lean_obj_tag(x_52)) {
+x_55 = l_Lean_Expr_getAppFn___main(x_53);
+switch (lean_obj_tag(x_55)) {
 case 1:
 {
-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_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_dec(x_3);
-x_53 = lean_ctor_get(x_52, 0);
-lean_inc(x_53);
-lean_dec(x_52);
-x_54 = lean_unsigned_to_nat(0u);
-x_55 = l_Lean_Expr_getAppNumArgsAux___main(x_50, x_54);
-lean_inc(x_55);
-x_56 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_56, 0, x_53);
-lean_ctor_set(x_56, 1, x_55);
-x_57 = lean_mk_empty_array_with_capacity(x_55);
+x_56 = lean_ctor_get(x_55, 0);
+lean_inc(x_56);
 lean_dec(x_55);
-x_58 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_50, x_57);
-x_59 = lean_alloc_ctor(0, 2, 0);
+x_57 = lean_unsigned_to_nat(0u);
+x_58 = l_Lean_Expr_getAppNumArgsAux___main(x_53, x_57);
+lean_inc(x_58);
+x_59 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_59, 0, x_56);
 lean_ctor_set(x_59, 1, x_58);
-x_60 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_60, 0, x_59);
-lean_ctor_set(x_60, 1, x_51);
-return x_60;
+x_60 = lean_mk_empty_array_with_capacity(x_58);
+lean_dec(x_58);
+x_61 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_53, x_60);
+x_62 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_62, 0, x_59);
+lean_ctor_set(x_62, 1, x_61);
+x_63 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_63, 0, x_62);
+lean_ctor_set(x_63, 1, x_54);
+return x_63;
 }
 case 2:
 {
-lean_dec(x_50);
+lean_dec(x_53);
 if (x_2 == 0)
 {
-lean_object* x_61; lean_object* x_62; 
-x_61 = lean_ctor_get(x_52, 0);
-lean_inc(x_61);
-lean_dec(x_52);
-x_62 = l_Lean_Meta_isReadOnlyOrSyntheticExprMVar(x_61, x_3, x_51);
+lean_object* x_64; uint8_t x_65; 
+x_64 = lean_ctor_get(x_3, 0);
+lean_inc(x_64);
+x_65 = lean_ctor_get_uint8(x_64, sizeof(void*)*1 + 3);
+lean_dec(x_64);
+if (x_65 == 0)
+{
+lean_object* x_66; lean_object* x_67; 
+x_66 = lean_ctor_get(x_55, 0);
+lean_inc(x_66);
+lean_dec(x_55);
+x_67 = l_Lean_Meta_isReadOnlyOrSyntheticExprMVar(x_66, x_3, x_54);
 lean_dec(x_3);
-if (lean_obj_tag(x_62) == 0)
+if (lean_obj_tag(x_67) == 0)
 {
-lean_object* x_63; uint8_t x_64; 
-x_63 = lean_ctor_get(x_62, 0);
-lean_inc(x_63);
-x_64 = lean_unbox(x_63);
-lean_dec(x_63);
-if (x_64 == 0)
+lean_object* x_68; uint8_t x_69; 
+x_68 = lean_ctor_get(x_67, 0);
+lean_inc(x_68);
+x_69 = lean_unbox(x_68);
+lean_dec(x_68);
+if (x_69 == 0)
 {
-lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; 
-x_65 = lean_ctor_get(x_62, 1);
-lean_inc(x_65);
-if (lean_is_exclusive(x_62)) {
- lean_ctor_release(x_62, 0);
- lean_ctor_release(x_62, 1);
- x_66 = x_62;
+lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; 
+x_70 = lean_ctor_get(x_67, 1);
+lean_inc(x_70);
+if (lean_is_exclusive(x_67)) {
+ lean_ctor_release(x_67, 0);
+ lean_ctor_release(x_67, 1);
+ x_71 = x_67;
 } else {
- lean_dec_ref(x_62);
- x_66 = lean_box(0);
+ lean_dec_ref(x_67);
+ x_71 = lean_box(0);
 }
-x_67 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__2;
-if (lean_is_scalar(x_66)) {
- x_68 = lean_alloc_ctor(0, 2, 0);
+x_72 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__2;
+if (lean_is_scalar(x_71)) {
+ x_73 = lean_alloc_ctor(0, 2, 0);
 } else {
- x_68 = x_66;
+ x_73 = x_71;
 }
-lean_ctor_set(x_68, 0, x_67);
-lean_ctor_set(x_68, 1, x_65);
-return x_68;
+lean_ctor_set(x_73, 0, x_72);
+lean_ctor_set(x_73, 1, x_70);
+return x_73;
 }
 else
 {
-lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; 
-x_69 = lean_ctor_get(x_62, 1);
-lean_inc(x_69);
-if (lean_is_exclusive(x_62)) {
- lean_ctor_release(x_62, 0);
- lean_ctor_release(x_62, 1);
- x_70 = x_62;
-} else {
- lean_dec_ref(x_62);
- x_70 = lean_box(0);
-}
-x_71 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
-if (lean_is_scalar(x_70)) {
- x_72 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_72 = x_70;
-}
-lean_ctor_set(x_72, 0, x_71);
-lean_ctor_set(x_72, 1, x_69);
-return x_72;
-}
-}
-else
-{
-lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; 
-x_73 = lean_ctor_get(x_62, 0);
-lean_inc(x_73);
-x_74 = lean_ctor_get(x_62, 1);
+lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; 
+x_74 = lean_ctor_get(x_67, 1);
 lean_inc(x_74);
-if (lean_is_exclusive(x_62)) {
- lean_ctor_release(x_62, 0);
- lean_ctor_release(x_62, 1);
- x_75 = x_62;
+if (lean_is_exclusive(x_67)) {
+ lean_ctor_release(x_67, 0);
+ lean_ctor_release(x_67, 1);
+ x_75 = x_67;
 } else {
- lean_dec_ref(x_62);
+ lean_dec_ref(x_67);
 x_75 = lean_box(0);
 }
+x_76 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
 if (lean_is_scalar(x_75)) {
- x_76 = lean_alloc_ctor(1, 2, 0);
+ x_77 = lean_alloc_ctor(0, 2, 0);
 } else {
- x_76 = x_75;
+ x_77 = x_75;
 }
-lean_ctor_set(x_76, 0, x_73);
-lean_ctor_set(x_76, 1, x_74);
-return x_76;
+lean_ctor_set(x_77, 0, x_76);
+lean_ctor_set(x_77, 1, x_74);
+return x_77;
 }
 }
 else
 {
-lean_object* x_77; lean_object* x_78; 
-lean_dec(x_52);
+lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; 
+x_78 = lean_ctor_get(x_67, 0);
+lean_inc(x_78);
+x_79 = lean_ctor_get(x_67, 1);
+lean_inc(x_79);
+if (lean_is_exclusive(x_67)) {
+ lean_ctor_release(x_67, 0);
+ lean_ctor_release(x_67, 1);
+ x_80 = x_67;
+} else {
+ lean_dec_ref(x_67);
+ x_80 = lean_box(0);
+}
+if (lean_is_scalar(x_80)) {
+ x_81 = lean_alloc_ctor(1, 2, 0);
+} else {
+ x_81 = x_80;
+}
+lean_ctor_set(x_81, 0, x_78);
+lean_ctor_set(x_81, 1, x_79);
+return x_81;
+}
+}
+else
+{
+lean_object* x_82; lean_object* x_83; 
+lean_dec(x_55);
 lean_dec(x_3);
-x_77 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
-x_78 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_78, 0, x_77);
-lean_ctor_set(x_78, 1, x_51);
-return x_78;
+x_82 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__2;
+x_83 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_83, 0, x_82);
+lean_ctor_set(x_83, 1, x_54);
+return x_83;
+}
+}
+else
+{
+lean_object* x_84; lean_object* x_85; 
+lean_dec(x_55);
+lean_dec(x_3);
+x_84 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
+x_85 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_85, 0, x_84);
+lean_ctor_set(x_85, 1, x_54);
+return x_85;
 }
 }
 case 4:
 {
-lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; 
+lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; 
 lean_dec(x_3);
-x_79 = lean_ctor_get(x_52, 0);
-lean_inc(x_79);
-lean_dec(x_52);
-x_80 = lean_unsigned_to_nat(0u);
-x_81 = l_Lean_Expr_getAppNumArgsAux___main(x_50, x_80);
-lean_inc(x_81);
-x_82 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_82, 0, x_79);
-lean_ctor_set(x_82, 1, x_81);
-x_83 = lean_mk_empty_array_with_capacity(x_81);
-lean_dec(x_81);
-x_84 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_50, x_83);
-x_85 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_85, 0, x_82);
-lean_ctor_set(x_85, 1, x_84);
-x_86 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_86, 0, x_85);
-lean_ctor_set(x_86, 1, x_51);
-return x_86;
+x_86 = lean_ctor_get(x_55, 0);
+lean_inc(x_86);
+lean_dec(x_55);
+x_87 = lean_unsigned_to_nat(0u);
+x_88 = l_Lean_Expr_getAppNumArgsAux___main(x_53, x_87);
+lean_inc(x_88);
+x_89 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_89, 0, x_86);
+lean_ctor_set(x_89, 1, x_88);
+x_90 = lean_mk_empty_array_with_capacity(x_88);
+lean_dec(x_88);
+x_91 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_53, x_90);
+x_92 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_92, 0, x_89);
+lean_ctor_set(x_92, 1, x_91);
+x_93 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_93, 0, x_92);
+lean_ctor_set(x_93, 1, x_54);
+return x_93;
 }
 case 9:
 {
-lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; 
-lean_dec(x_50);
+lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; 
+lean_dec(x_53);
 lean_dec(x_3);
-x_87 = lean_ctor_get(x_52, 0);
-lean_inc(x_87);
-lean_dec(x_52);
-x_88 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_88, 0, x_87);
-x_89 = l_Array_empty___closed__1;
-x_90 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_90, 0, x_88);
-lean_ctor_set(x_90, 1, x_89);
-x_91 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_91, 0, x_90);
-lean_ctor_set(x_91, 1, x_51);
-return x_91;
+x_94 = lean_ctor_get(x_55, 0);
+lean_inc(x_94);
+lean_dec(x_55);
+x_95 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_95, 0, x_94);
+x_96 = l_Array_empty___closed__1;
+x_97 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_97, 0, x_95);
+lean_ctor_set(x_97, 1, x_96);
+x_98 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_98, 0, x_97);
+lean_ctor_set(x_98, 1, x_54);
+return x_98;
 }
 default: 
 {
-lean_object* x_92; lean_object* x_93; 
-lean_dec(x_52);
-lean_dec(x_50);
+lean_object* x_99; lean_object* x_100; 
+lean_dec(x_55);
+lean_dec(x_53);
 lean_dec(x_3);
-x_92 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
-x_93 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_93, 0, x_92);
-lean_ctor_set(x_93, 1, x_51);
-return x_93;
+x_99 = l___private_Init_Lean_Meta_DiscrTree_11__getKeyArgs___closed__1;
+x_100 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_100, 0, x_99);
+lean_ctor_set(x_100, 1, x_54);
+return x_100;
 }
 }
 }
 }
 else
 {
-uint8_t x_94; 
+uint8_t x_101; 
 lean_dec(x_3);
-x_94 = !lean_is_exclusive(x_5);
-if (x_94 == 0)
+x_101 = !lean_is_exclusive(x_5);
+if (x_101 == 0)
 {
 return x_5;
 }
 else
 {
-lean_object* x_95; lean_object* x_96; lean_object* x_97; 
-x_95 = lean_ctor_get(x_5, 0);
-x_96 = lean_ctor_get(x_5, 1);
-lean_inc(x_96);
-lean_inc(x_95);
+lean_object* x_102; lean_object* x_103; lean_object* x_104; 
+x_102 = lean_ctor_get(x_5, 0);
+x_103 = lean_ctor_get(x_5, 1);
+lean_inc(x_103);
+lean_inc(x_102);
 lean_dec(x_5);
-x_97 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_97, 0, x_95);
-lean_ctor_set(x_97, 1, x_96);
-return x_97;
+x_104 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_104, 0, x_102);
+lean_ctor_set(x_104, 1, x_103);
+return x_104;
 }
 }
 }
--- a/stage0/stdlib/Init/Lean/Meta/FunInfo.c
+++ b/stage0/stdlib/Init/Lean/Meta/FunInfo.c
@ -9168,6 +9168,8 @@ _start:
 lean_object* x_9; 
 if (lean_obj_tag(x_6) == 7)
 {
+if (lean_obj_tag(x_2) == 0)
+{
 lean_object* x_22; lean_object* x_23; lean_object* x_24; uint64_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; 
 x_22 = lean_ctor_get(x_6, 0);
 lean_inc(x_22);
@ -9193,8 +9195,6 @@ lean_inc(x_29);
 x_32 = lean_local_ctx_mk_local_decl(x_3, x_29, x_22, x_27, x_31);
 x_33 = l_Lean_mkFVar(x_29);
 x_34 = lean_array_push(x_4, x_33);
-if (lean_obj_tag(x_2) == 0)
-{
 x_3 = x_32;
 x_4 = x_34;
 x_6 = x_24;
@ -9203,65 +9203,91 @@ goto _start;
 }
 else
 {
-lean_object* x_36; lean_object* x_37; uint8_t x_38; 
-x_36 = lean_ctor_get(x_2, 0);
+lean_object* x_36; lean_object* x_37; lean_object* x_38; uint64_t x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; 
+x_36 = lean_ctor_get(x_6, 0);
 lean_inc(x_36);
-x_37 = lean_array_get_size(x_34);
-x_38 = lean_nat_dec_lt(x_37, x_36);
+x_37 = lean_ctor_get(x_6, 1);
+lean_inc(x_37);
+x_38 = lean_ctor_get(x_6, 2);
+lean_inc(x_38);
+x_39 = lean_ctor_get_uint64(x_6, sizeof(void*)*3);
+x_40 = lean_ctor_get(x_2, 0);
+lean_inc(x_40);
+x_41 = lean_array_get_size(x_4);
+x_42 = lean_nat_dec_lt(x_41, x_40);
+lean_dec(x_40);
+if (x_42 == 0)
+{
+lean_object* x_43; uint8_t x_44; 
+lean_dec(x_38);
+lean_dec(x_37);
 lean_dec(x_36);
-if (x_38 == 0)
-{
-lean_object* x_39; uint8_t x_40; 
 lean_dec(x_2);
-lean_inc(x_34);
-x_39 = lean_expr_instantiate_rev_range(x_24, x_5, x_37, x_34);
-lean_dec(x_24);
-x_40 = !lean_is_exclusive(x_7);
-if (x_40 == 0)
+lean_inc(x_4);
+x_43 = lean_expr_instantiate_rev_range(x_6, x_5, x_41, x_4);
+lean_dec(x_6);
+x_44 = !lean_is_exclusive(x_7);
+if (x_44 == 0)
 {
-lean_object* x_41; lean_object* x_42; 
-x_41 = lean_ctor_get(x_7, 1);
-lean_dec(x_41);
-lean_ctor_set(x_7, 1, x_32);
-x_42 = l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_FunInfo_6__getFunInfoAux___spec__6(x_34, x_37, x_39, x_34, x_5, x_7, x_30);
-lean_dec(x_39);
-lean_dec(x_34);
-return x_42;
-}
-else
-{
-lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; 
-x_43 = lean_ctor_get(x_7, 0);
-x_44 = lean_ctor_get(x_7, 2);
-lean_inc(x_44);
-lean_inc(x_43);
-lean_dec(x_7);
-x_45 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_45, 0, x_43);
-lean_ctor_set(x_45, 1, x_32);
-lean_ctor_set(x_45, 2, x_44);
-x_46 = l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_FunInfo_6__getFunInfoAux___spec__6(x_34, x_37, x_39, x_34, x_5, x_45, x_30);
-lean_dec(x_39);
-lean_dec(x_34);
+lean_object* x_45; lean_object* x_46; 
+x_45 = lean_ctor_get(x_7, 1);
+lean_dec(x_45);
+lean_ctor_set(x_7, 1, x_3);
+x_46 = l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_FunInfo_6__getFunInfoAux___spec__6(x_4, x_41, x_43, x_4, x_5, x_7, x_8);
+lean_dec(x_43);
+lean_dec(x_4);
 return x_46;
 }
+else
+{
+lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; 
+x_47 = lean_ctor_get(x_7, 0);
+x_48 = lean_ctor_get(x_7, 2);
+lean_inc(x_48);
+lean_inc(x_47);
+lean_dec(x_7);
+x_49 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_49, 0, x_47);
+lean_ctor_set(x_49, 1, x_3);
+lean_ctor_set(x_49, 2, x_48);
+x_50 = l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_FunInfo_6__getFunInfoAux___spec__6(x_4, x_41, x_43, x_4, x_5, x_49, x_8);
+lean_dec(x_43);
+lean_dec(x_4);
+return x_50;
+}
 }
 else
 {
+lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; uint8_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; 
+lean_dec(x_6);
+lean_inc(x_4);
+x_51 = lean_expr_instantiate_rev_range(x_37, x_5, x_41, x_4);
+lean_dec(x_41);
 lean_dec(x_37);
-x_3 = x_32;
-x_4 = x_34;
-x_6 = x_24;
-x_8 = x_30;
+x_52 = l_Lean_Meta_mkFreshId___rarg(x_8);
+x_53 = lean_ctor_get(x_52, 0);
+lean_inc(x_53);
+x_54 = lean_ctor_get(x_52, 1);
+lean_inc(x_54);
+lean_dec(x_52);
+x_55 = (uint8_t)((x_39 << 24) >> 61);
+lean_inc(x_53);
+x_56 = lean_local_ctx_mk_local_decl(x_3, x_53, x_36, x_51, x_55);
+x_57 = l_Lean_mkFVar(x_53);
+x_58 = lean_array_push(x_4, x_57);
+x_3 = x_56;
+x_4 = x_58;
+x_6 = x_38;
+x_8 = x_54;
 goto _start;
 }
 }
 }
 else
 {
-lean_object* x_48; 
-x_48 = lean_box(0);
-x_9 = x_48;
+lean_object* x_60; 
+x_60 = lean_box(0);
+x_9 = x_60;
 goto block_21;
 }
 block_21:
--- a/stage0/stdlib/Init/Lean/Structure.c
+++ b/stage0/stdlib/Init/Lean/Structure.c
--- a/stage0/stdlib/Init/Lean/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Syntax.c
@ -15,10 +15,12 @@ extern "C" {
 #endif
 lean_object* l_Lean_Syntax_reprint___main___closed__1;
 lean_object* l_Lean_Syntax_reprint___main___boxed(lean_object*);
+lean_object* l_Lean_Syntax_isIdOrAtom_x3f___boxed(lean_object*);
 lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf(lean_object*, lean_object*);
 lean_object* l_Lean_fieldIdxKind;
+lean_object* l_Lean_Syntax_isNatLit_x3f___boxed(lean_object*);
 lean_object* l___private_Init_Lean_Syntax_1__updateInfo(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_setTailInfoAux(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Syntax_6__decodeOctalLitAux(lean_object*, lean_object*, lean_object*);
@ -49,7 +51,6 @@ lean_object* l_Lean_Syntax_mreplace___main___boxed(lean_object*);
 uint8_t l_Char_isDigit(uint32_t);
 lean_object* l_Lean_charLitKind___closed__2;
 uint8_t lean_name_eq(lean_object*, lean_object*);
-lean_object* l_Lean_Syntax_isStrLit___boxed(lean_object*);
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_reprint___main(lean_object*);
@ -61,7 +62,6 @@ lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_charLitKind___closed__1;
-lean_object* l_Lean_Syntax_isNatLit___boxed(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_setAtomVal(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_setTailInfo(lean_object*, lean_object*);
@ -90,7 +90,6 @@ lean_object* l_Lean_SyntaxNode_getArgs(lean_object*);
 lean_object* l_Lean_Syntax_getKind___boxed(lean_object*);
 lean_object* l_Lean_Syntax_rewriteBottomUp(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___main(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Syntax_isNatLit(lean_object*);
 lean_object* lean_string_utf8_next(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_ifNode(lean_object*);
 lean_object* lean_mk_syntax_ident(lean_object*);
@ -100,6 +99,7 @@ lean_object* l_Lean_SyntaxNode_getIdAt(lean_object*, lean_object*);
 lean_object* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStx___main___spec__2___boxed(lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Lean_SyntaxNode_getKind___boxed(lean_object*);
+lean_object* l_Lean_Syntax_isNatLit_x3f(lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_updateTrailing(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_formatStx___main___closed__3;
@ -110,8 +110,10 @@ lean_object* l_Lean_Syntax_mreplace___main___rarg(lean_object*, lean_object*, le
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_choiceKind___closed__2;
 lean_object* l_Lean_strLitKind;
+lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getId___boxed(lean_object*);
+lean_object* l_Lean_Syntax_isFieldIdx_x3f(lean_object*);
 lean_object* l_Lean_Syntax_formatStx___main___closed__7;
 lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
@ -131,7 +133,6 @@ lean_object* l_Lean_Syntax_setArgs(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_repr(lean_object*);
 lean_object* l_Lean_Syntax_getId(lean_object*);
-lean_object* l_Lean_Syntax_isStrLit(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_choiceKind;
 lean_object* l_Lean_charLitKind;
@ -163,6 +164,7 @@ lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1___boxed(le
 lean_object* l_Lean_Syntax_updateTrailing___main(lean_object*, lean_object*);
 lean_object* l_Lean_nullKind___closed__2;
 extern lean_object* l_Lean_Format_sbracket___closed__3;
+lean_object* l_Lean_Syntax_isStrLit_x3f___boxed(lean_object*);
 lean_object* l___private_Init_Lean_Syntax_6__decodeOctalLitAux___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_syntax_atom(lean_object*);
 lean_object* l_Lean_unreachIsNodeAtom(lean_object*, lean_object*, lean_object*, lean_object*);
@ -172,6 +174,7 @@ lean_object* l_Lean_Syntax_getHeadInfo___main(lean_object*);
 extern lean_object* l_Lean_formatDataValue___closed__2;
 uint8_t l_Lean_Syntax_isMissing(lean_object*);
 lean_object* l_Array_umapMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_isIdOrAtom_x3f(lean_object*);
 extern lean_object* l_Lean_HasRepr___closed__1;
 lean_object* l_Lean_Syntax_setArg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SourceInfo_appendToTrailing(lean_object*, lean_object*);
@ -206,7 +209,6 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__
 lean_object* l_Array_umapMAux___main___at_Lean_Syntax_updateLeading___spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_HasToString___closed__1;
 lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Syntax_isIdOrAtom___boxed(lean_object*);
 lean_object* l_Lean_mkOptionalNode___closed__1;
 lean_object* l_Lean_Syntax_mrewriteBottomUp___main(lean_object*);
 lean_object* l_Lean_SyntaxNode_getIdAt___boxed(lean_object*, lean_object*);
@ -214,7 +216,6 @@ lean_object* l_Lean_Syntax_getTailInfo(lean_object*);
 lean_object* l_Lean_Syntax_formatStx___main(lean_object*);
 lean_object* l_Array_toList___rarg(lean_object*);
 lean_object* l_Lean_Syntax_mrewriteBottomUp___main___at_Lean_Syntax_rewriteBottomUp___spec__1(lean_object*, lean_object*);
-lean_object* l_Lean_Syntax_isIdOrAtom(lean_object*);
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 lean_object* lean_mk_syntax_list(lean_object*);
 lean_object* l___private_Init_Lean_Syntax_8__decodeDecimalLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
@ -239,7 +240,6 @@ lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*
 lean_object* l_Lean_mkAtomFrom___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Syntax_isFieldIdx(lean_object*);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
 lean_object* l_Lean_Syntax_ifNodeKind___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_formatStx___main___closed__1;
@ -252,7 +252,7 @@ lean_object* l_Lean_Syntax_getTailInfo___main(lean_object*);
 lean_object* l_Lean_Syntax_formatStx___main___closed__8;
 lean_object* l___private_Init_Lean_Syntax_9__decodeNatLitVal___closed__1;
 lean_object* l_Lean_SyntaxNode_getArg(lean_object*, lean_object*);
-lean_object* l_Lean_Syntax_isFieldIdx___boxed(lean_object*);
+lean_object* l_Lean_Syntax_isFieldIdx_x3f___boxed(lean_object*);
 lean_object* l_Lean_Syntax_reprint(lean_object*);
 lean_object* l___private_Init_Lean_Syntax_6__decodeOctalLitAux___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -4110,7 +4110,7 @@ x_5 = l_Lean_mkStxLit(x_4, x_2, x_3);
 return x_5;
 }
 }
-lean_object* l_Lean_Syntax_isStrLit(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object* x_1) {
 _start:
 {
 if (lean_obj_tag(x_1) == 1)
@ -4173,11 +4173,11 @@ return x_17;
 }
 }
 }
-lean_object* l_Lean_Syntax_isStrLit___boxed(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isStrLit_x3f___boxed(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = l_Lean_Syntax_isStrLit(x_1);
+x_2 = l_Lean_Syntax_isStrLit_x3f(x_1);
 lean_dec(x_1);
 return x_2;
 }
@ -4929,7 +4929,7 @@ lean_dec(x_1);
 return x_3;
 }
 }
-lean_object* l_Lean_Syntax_isNatLit(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isNatLit_x3f(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@ -4938,16 +4938,16 @@ x_3 = l_Lean_Syntax_isNatLitAux(x_2, x_1);
 return x_3;
 }
 }
-lean_object* l_Lean_Syntax_isNatLit___boxed(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isNatLit_x3f___boxed(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = l_Lean_Syntax_isNatLit(x_1);
+x_2 = l_Lean_Syntax_isNatLit_x3f(x_1);
 lean_dec(x_1);
 return x_2;
 }
 }
-lean_object* l_Lean_Syntax_isFieldIdx(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isFieldIdx_x3f(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@ -4956,16 +4956,16 @@ x_3 = l_Lean_Syntax_isNatLitAux(x_2, x_1);
 return x_3;
 }
 }
-lean_object* l_Lean_Syntax_isFieldIdx___boxed(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isFieldIdx_x3f___boxed(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = l_Lean_Syntax_isFieldIdx(x_1);
+x_2 = l_Lean_Syntax_isFieldIdx_x3f(x_1);
 lean_dec(x_1);
 return x_2;
 }
 }
-lean_object* l_Lean_Syntax_isIdOrAtom(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isIdOrAtom_x3f(lean_object* x_1) {
 _start:
 {
 switch (lean_obj_tag(x_1)) {
@ -4999,11 +4999,11 @@ return x_10;
 }
 }
 }
-lean_object* l_Lean_Syntax_isIdOrAtom___boxed(lean_object* x_1) {
+lean_object* l_Lean_Syntax_isIdOrAtom_x3f___boxed(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = l_Lean_Syntax_isIdOrAtom(x_1);
+x_2 = l_Lean_Syntax_isIdOrAtom_x3f(x_1);
 lean_dec(x_1);
 return x_2;
 }