chore: update stage0

2020-07-23 16:46:52 -07:00 · 2020-07-23 16:46:52 -07:00 · b5977d9c06
commit b5977d9c06
parent be06ce5fec
18 changed files with 4317 additions and 2880 deletions
--- a/stage0/src/Lean/Elab/ResolveName.lean
+++ b/stage0/src/Lean/Elab/ResolveName.lean
@ -88,6 +88,8 @@ private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : Li
  | some newId => [(newId, projs)]
  | none =>
  let resolvedIds := if env.contains id then [id] else [];
+  let idPrv := mkPrivateName env id;
+  let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds;
  let resolvedIds := resolveOpenDecls env id openDecls resolvedIds;
  let resolvedIds := getAliases env id ++ resolvedIds;
  match resolvedIds with
--- a/stage0/src/Lean/Elab/Structure.lean
+++ b/stage0/src/Lean/Elab/Structure.lean
@ -54,13 +54,29 @@ inductive StructFieldKind
 | newField | fromParent | subobject

 structure StructFieldInfo :=
-(name   : Name)
-(fvar   : Expr)
-(kind   : StructFieldKind)
-(value? : Option Expr := none)
+(name     : Name)
+(declName : Name) -- Remark: this field value doesn't matter for fromParent fields.
+(fvar     : Expr)
+(kind     : StructFieldKind)
+(inferMod : Bool := false)
+(value?   : Option Expr := none)
+
+instance StructFieldInfo.inhabited : Inhabited StructFieldInfo :=
+⟨{ name := arbitrary _, declName := arbitrary _, fvar := arbitrary _, kind := StructFieldKind.newField }⟩
+
+def StructFieldInfo.isFromParent (info : StructFieldInfo) : Bool :=
+match info.kind with
+| StructFieldKind.fromParent => true
+| _                          => false
+
+/- Auxiliary declaration for `mkProjections` -/
+structure ProjectionInfo :=
+(declName : Name)
+(inferMod : Bool)

 structure ElabStructResult :=
 (decl      : Declaration)
+(projInfos : List ProjectionInfo)

 private def defaultCtorName := `mk

@ -70,19 +86,23 @@ The structore constructor syntax is
 parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
 ```
 -/
-private def expandCtor (structStx : Syntax) (structDeclName : Name) : CommandElabM StructCtorView :=
+private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM StructCtorView :=
 let optCtor := structStx.getArg 6;
 if optCtor.isNone then
  pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName }
 else do
  let ctor := optCtor.getArg 0;
-  modifiers ← elabModifiers (ctor.getArg 0);
-  checkValidCtorModifier ctor modifiers;
+  ctorModifiers ← elabModifiers (ctor.getArg 0);
+  checkValidCtorModifier ctor ctorModifiers;
+  when (ctorModifiers.isPrivate && structModifiers.isPrivate) $
+    throwError ctor "invalid 'private' constructor in a 'private' structure";
+  when (ctorModifiers.isProtected && structModifiers.isPrivate) $
+    throwError ctor "invalid 'protected' constructor in a 'private' structure";
  let inferMod := !(ctor.getArg 2).isNone;
  let name := ctor.getIdAt 1;
  let declName := structDeclName ++ name;
-  declName ← applyVisibility ctor modifiers.visibility declName;
-  pure { ref := ctor, name := name, modifiers := modifiers, inferMod := inferMod, declName := declName }
+  declName ← applyVisibility ctor ctorModifiers.visibility declName;
+  pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }

 def checkValidFieldModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
 when modifiers.isNoncomputable $
@ -105,7 +125,7 @@ def structInstBinder     := parser! try (declModifiers >> "[") >> many1 ident >>
 def structFields         := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
 ```
 -/
-private def expandFields (structStx : Syntax) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
+private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
 let fieldBinders := ((structStx.getArg 7).getArg 0).getArgs;
 fieldBinders.foldlM
  (fun (views : Array StructFieldView) fieldBinder => do
@ -115,8 +135,12 @@ fieldBinders.foldlM
      else if k == `Lean.Parser.Command.structImplicitBinder then pure BinderInfo.implicit
      else if k == `Lean.Parser.Command.structInstBinder then pure BinderInfo.instImplicit
      else throwError fieldBinder "unexpected kind of structure field";
-    modifiers ← elabModifiers (fieldBinder.getArg 0);
-    checkValidFieldModifier fieldBinder modifiers;
+    fieldModifiers ← elabModifiers (fieldBinder.getArg 0);
+    checkValidFieldModifier fieldBinder fieldModifiers;
+    when (fieldModifiers.isPrivate && structModifiers.isPrivate) $
+      throwError fieldBinder "invalid 'private' field in a 'private' structure";
+    when (fieldModifiers.isProtected && structModifiers.isPrivate) $
+      throwError fieldBinder "invalid 'protected' field in a 'private' structure";
    let inferMod         := !(fieldBinder.getArg 3).isNone;
    let (binders, type?) :=
      if binfo == BinderInfo.default then
@ -139,10 +163,10 @@ fieldBinders.foldlM
        when (isInternalSubobjectFieldName name) $
          throwError ident ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
        let declName := structDeclName ++ name;
-        declName ← applyVisibility ident modifiers.visibility declName;
+        declName ← applyVisibility ident fieldModifiers.visibility declName;
        pure $ views.push {
          ref        := ident,
-          modifiers  := modifiers,
+          modifiers  := fieldModifiers,
          binderInfo := binfo,
          inferMod   := inferMod,
          declName   := declName,
@ -184,7 +208,7 @@ private partial def processSubfields {α} (ref : Syntax) (parentFVar : Expr) (pa
    val  ← Term.liftMetaM ref $ Meta.mkProjection parentFVar subfieldName;
    type ← Term.inferType ref val;
    Term.withLetDecl ref subfieldName type val fun subfieldFVar =>
-      let infos := infos.push { name := subfieldName, fvar := subfieldFVar, kind := StructFieldKind.fromParent };
+      let infos := infos.push { name := subfieldName, declName := arbitrary _, fvar := subfieldFVar, kind := StructFieldKind.fromParent };
      processSubfields (i+1) infos k
  else
    k infos
@ -201,7 +225,7 @@ private partial def withParents {α} (view : StructView) : Nat → Array StructF
    env ← Term.getEnv;
    let binfo := if view.isClass && isClass env parentName then BinderInfo.instImplicit else BinderInfo.default;
    Term.withLocalDecl parentStx toParentName binfo parent $ fun parentFVar =>
-      let infos := infos.push { name := toParentName, fvar := parentFVar, kind := StructFieldKind.subobject };
+      let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject };
      let subfieldNames := getStructureFieldsFlattened env parentName;
      processSubfields parentStx parentFVar parentName subfieldNames 0 infos fun infos => withParents (i+1) infos k
  else
@ -231,12 +255,13 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
      | none,      none => Term.throwError view.ref "invalid field, type expected"
      | some type, _    =>
        Term.withLocalDecl view.ref view.name view.binderInfo type $ fun fieldFVar =>
-          let infos := infos.push { name := view.name, fvar := fieldFVar, value? := value?, kind := StructFieldKind.newField };
+          let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, value? := value?,
+                                    kind := StructFieldKind.newField, inferMod := view.inferMod };
          withFields (i+1) infos k
      | none, some value => do
        type ← Term.inferType view.ref value;
        Term.withLocalDecl view.ref view.name view.binderInfo type $ fun fieldFVar =>
-          let infos := infos.push { name := view.name, fvar := fieldFVar, kind := StructFieldKind.newField };
+          let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, kind := StructFieldKind.newField, inferMod := view.inferMod };
          withFields (i+1) infos k
    | some info =>
      match info.kind with
@ -342,6 +367,30 @@ s ← collectLevelParamsInFVars ref params s;
 s ← fieldInfos.foldlM (fun (s : CollectLevelParams.State) info => collectLevelParamsInFVar ref s info.fvar) s;
 pure s.params

+private def addCtorFields (ref : Syntax) (fieldInfos : Array StructFieldInfo) : Nat → Expr → TermElabM Expr
+| 0,   type => pure type
+| i+1, type => do
+  let info := fieldInfos.get! i;
+  decl ← Term.getFVarLocalDecl! info.fvar;
+  let type := type.abstract #[info.fvar];
+  match info.kind with
+  | StructFieldKind.fromParent =>
+    let val := decl.value;
+    addCtorFields i (type.instantiate1 val)
+  | StructFieldKind.subobject =>
+    let n := mkInternalSubobjectFieldName $ decl.userName;
+    addCtorFields i (mkForall n decl.binderInfo decl.type type)
+  | StructFieldKind.newField =>
+    addCtorFields i (mkForall decl.userName decl.binderInfo decl.type type)
+
+private def mkCtor (view : StructView) (levelParams : List Name) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Constructor := do
+let type := mkAppN (mkConst view.declName (levelParams.map mkLevelParam)) params;
+type ← addCtorFields view.ref fieldInfos fieldInfos.size type;
+type ← Term.mkForall view.ref params type;
+type ← Term.instantiateMVars view.ref type;
+let type := type.inferImplicit params.size !view.ctor.inferMod;
+pure { name := view.ctor.declName, type := type }
+
 private def elabStructureView (view : StructView) : TermElabM ElabStructResult := do
 let numExplicitParams := view.params.size;
 type ← Term.elabType view.type;
@ -360,10 +409,25 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
    match sortDeclLevelParams view.scopeLevelNames view.allUserLevelNames usedLevelNames with
    | Except.error msg      => Term.throwError ref msg
    | Except.ok levelParams => do
-      structType ← Term.mkForall ref view.params type;
-      structType ← Term.mkForall ref scopeVars structType;
-      -- TODO
-      Term.throwError view.ref ("WIP " ++ toString levelParams ++ " " ++ structType)
+      let params := scopeVars ++ view.params;
+      ctor ← mkCtor view levelParams params fieldInfos;
+      type ← Term.mkForall ref view.params type;
+      type ← Term.mkForall ref scopeVars type;
+      type ← Term.instantiateMVars ref type;
+      let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType };
+      let decl    := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe;
+      let projInfos := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) =>
+        { declName := info.declName, inferMod := info.inferMod : ProjectionInfo };
+      pure { decl := decl, projInfos := projInfos }
+
+@[extern "lean_mk_projections"]
+private constant mkProjections (env : Environment) (structName : @& Name) (projs : @& List ProjectionInfo) (isClass : Bool) : Except String Environment := arbitrary _
+
+private def addProjections (ref : Syntax) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : CommandElabM Unit := do
+env ← getEnv;
+match mkProjections env structName projs isClass with
+| Except.ok env    => setEnv env
+| Except.error msg => throwError ref msg

 /-
 parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields
@ -391,8 +455,8 @@ scopeLevelNames ← getLevelNames;
 withDeclId declId $ fun name => do
  declName ← mkDeclName declId modifiers name;
  allUserLevelNames ← getLevelNames;
-  ctor ← expandCtor stx declName;
-  fields ← expandFields stx declName;
+  ctor ← expandCtor stx modifiers declName;
+  fields ← expandFields stx modifiers declName;
  r ← runTermElabM declName $ fun scopeVars => Term.elabBinders params $ fun params => elabStructureView {
    ref               := stx,
    modifiers         := modifiers,
@ -407,7 +471,13 @@ withDeclId declId $ fun name => do
    ctor              := ctor,
    fields            := fields
  };
-  pure () -- TODO
+  let ref := declId;
+  addDecl ref r.decl;
+  addProjections ref declName r.projInfos isClass;
+  -- TODO: add auxiliary definitions recOn and casesOn
+  -- TODO: register default values
+  -- TODO: add coercions
+  pure ()

 end Command
 end Elab
--- a/stage0/src/Lean/Elab/Term.lean
+++ b/stage0/src/Lean/Elab/Term.lean
@ -124,6 +124,12 @@ def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx
 def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances
 def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts
 def getLevelNames : TermElabM (List Name) := do ctx ← read; pure ctx.levelNames
+def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
+  lctx ← getLCtx;
+  match lctx.find? fvar.fvarId! with
+  | some d => pure d
+  | none   => unreachable!
+
 def setEnv (env : Environment) : TermElabM Unit := modify $ fun s => { s with env := env }
 def setMCtx (mctx : MetavarContext) : TermElabM Unit := modify $ fun s => { s with mctx := mctx }

--- a/stage0/src/frontends/lean/pp.cpp
+++ b/stage0/src/frontends/lean/pp.cpp
@ -685,7 +685,7 @@ static bool is_structure_instance(environment const & env, expr const & e, bool
    if (!is_constant(fn)) return false;
    name const & mk_name = const_name(fn);
    if (!is_constructor(env, mk_name)) return false;
-    name const & S       = mk_name.get_prefix();
+    name S = get_constructor_inductive_type(env, mk_name);
    if (!is_structure(env, S)) return false;
    /* If implicit arguments is true, and the structure has parameters, we should not
       pretty print using { ... }, because we will not be able to see the parameters. */
--- a/stage0/src/library/constructions/projection.cpp
+++ b/stage0/src/library/constructions/projection.cpp
@ -110,6 +110,25 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
    return new_env;
 }

+
+extern "C" object * lean_mk_projections(object * env, object * struct_name, object * proj_infos, uint8 inst_implicit) {
+    environment new_env(env);
+    name n(struct_name, true);
+    list_ref<object_ref> ps(proj_infos, true);
+    buffer<name> proj_names;
+    buffer<implicit_infer_kind> infer_kinds;
+    for (auto p : ps) {
+        proj_names.push_back(cnstr_get_ref_t<name>(p, 0));
+        infer_kinds.push_back(unbox(cnstr_get_ref(p, 1).raw()) == 0 ? implicit_infer_kind::RelaxedImplicit : implicit_infer_kind::Implicit);
+    }
+    try {
+        new_env = mk_projections(new_env, n, proj_names, infer_kinds, inst_implicit != 0);
+        return mk_except_ok(new_env);
+    } catch (exception & ex) {
+        return mk_except_error(string_ref(ex.what()));
+    }
+}
+
 void initialize_def_projection() {
 }

--- a/stage0/src/library/util.cpp
+++ b/stage0/src/library/util.cpp
@ -318,6 +318,13 @@ unsigned get_constructor_idx(environment const & env, name const & n) {
    lean_unreachable();
 }

+name get_constructor_inductive_type(environment const & env, name const & ctor_name) {
+    constant_info info  = env.get(ctor_name);
+    lean_assert(info.is_constructor());
+    constructor_val val = info.to_constructor_val();
+    return val.get_induct();
+}
+
 expr instantiate_lparam(expr const & e, name const & p, level const & l) {
    return instantiate_lparams(e, names(p), levels(l));
 }
--- a/stage0/src/library/util.h
+++ b/stage0/src/library/util.h
@ -124,6 +124,11 @@ unsigned get_num_constructors(environment const & env, name const & n);
    \pre inductive::is_intro_rule(env, n) */
 unsigned get_constructor_idx(environment const & env, name const & n);

+/** \brief Given a constructor name, return the associated inductive type name.
+
+    \pre inductive::is_intro_rule(env, ctor_name) */
+name get_constructor_inductive_type(environment const & env, name const & ctor_name);
+
 /** \brief Given an expression \c e, return the number of arguments expected arguments.

    \remark This function counts the number of nested Pi's in \c e. Weak-head-normal-forms are computed for the type of \c e.
--- a/stage0/stdlib/Lean/Elab/App.c
+++ b/stage0/stdlib/Lean/Elab/App.c
@ -234,7 +234,6 @@ lean_object* l___private_Lean_Elab_App_17__addLValArg___main___closed__11;
 lean_object* l_Lean_Elab_Term_elabApp(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getPathToBaseStructure_x3f(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeAppInstMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
 lean_object* l___private_Lean_Elab_App_4__tryCoeFun___closed__3;
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 uint8_t l_Array_isEmpty___rarg(lean_object*);
@ -251,6 +250,7 @@ extern lean_object* l_Lean_Elab_Term_TermElabResult_inhabited;
 lean_object* l_List_map___main___at___private_Lean_Elab_App_20__elabAppFnId___spec__1(lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_App_24__mergeFailures___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
+extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabProj___closed__1;
 lean_object* l___private_Lean_Elab_App_4__tryCoeFun___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_isAutoParam(lean_object*);
@ -16952,7 +16952,7 @@ if (lean_obj_tag(x_13) == 0)
 {
 lean_object* x_14; lean_object* x_15; lean_object* x_16; 
 lean_dec(x_13);
-x_14 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
+x_14 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_15 = l_unreachable_x21___rarg(x_14);
 lean_inc(x_4);
 x_16 = lean_apply_2(x_15, x_4, x_5);
--- a/stage0/stdlib/Lean/Elab/Binders.c
+++ b/stage0/stdlib/Lean/Elab/Binders.c
@ -24,10 +24,12 @@ lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__13;
 lean_object* l_Lean_Elab_Term_elabLetDecl(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_4__expandBinderModifier___closed__3;
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__12;
 extern lean_object* l___private_Lean_Meta_ExprDefEq_8__checkTypesAndAssign___closed__7;
 lean_object* l_Lean_Elab_Term_elabDepArrow___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabForall___closed__1;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__10;
 lean_object* l_unreachable_x21___rarg(lean_object*);
 extern lean_object* l_Lean_nullKind;
 lean_object* l___private_Lean_Syntax_7__quoteName___main(lean_object*);
@ -43,7 +45,6 @@ lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__3(lean_object*, lean_obje
 lean_object* l_Lean_Elab_Term_elabBinder___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabFun(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__2;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__26;
 extern lean_object* l_Lean_identKind___closed__2;
 lean_object* l_Lean_Elab_Term_elabForall___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__1;
@ -72,7 +73,6 @@ lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 extern lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__2;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabFun(lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__11;
 lean_object* l___private_Lean_Elab_Binders_7__elabBinderViews(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Binders_11__expandFunBindersAux___main___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareTacticSyntax___closed__3;
@ -98,10 +98,10 @@ lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Binders_6__matchBi
 lean_object* l_Lean_Elab_Term_getOptions(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 lean_object* l_Lean_Syntax_isSimpleTermId_x3f(lean_object*, uint8_t);
 lean_object* l_Lean_Elab_Term_FunBinders_elabFunBindersAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__3;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__8;
 lean_object* l___private_Lean_Elab_Binders_11__expandFunBindersAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_getOptParamDefault_x3f___closed__2;
@ -112,7 +112,6 @@ lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__1;
 lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshFVarId___rarg(lean_object*);
 lean_object* l___private_Lean_Elab_Binders_4__expandBinderModifier___closed__2;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__4;
 lean_object* l_Lean_Elab_Term_declareTacticSyntax(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*);
 extern lean_object* l_Lean_Parser_Term_implicitBinder___elambda__1___closed__1;
@ -153,28 +152,25 @@ lean_object* l_Lean_Elab_Term_elabFunBinders(lean_object*);
 extern lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__1;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Binders_6__matchBinder___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__21;
 extern lean_object* l___private_Lean_Meta_ExprDefEq_8__checkTypesAndAssign___closed__8;
 lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Elab_Term_5__expandCDot___main___closed__4;
 extern lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_elabBinder___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__23;
 lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_2__expandBinderIdent___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__2;
 lean_object* l___private_Lean_Elab_Binders_10__getFunBinderIds_x3f(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_13__propagateExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__13;
 lean_object* l___private_Lean_Elab_Binders_14__elabFunBinderViews___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandOptType(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withLocalDecl___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_12__checkNoOptAutoParam(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabForall(lean_object*);
 extern lean_object* l_Lean_mkAppStx___closed__6;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
 lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__6;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
 lean_object* l___private_Lean_Elab_Binders_9__getFunBinderIdsAux_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Quotation_2__quoteSyntax___main___spec__1___closed__3;
 lean_object* l___private_Lean_Elab_Binders_9__getFunBinderIdsAux_x3f(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
@ -197,7 +193,7 @@ lean_object* l_Lean_Elab_Term_elabLetBangDecl___closed__1;
 lean_object* l_Lean_mkFVar(lean_object*);
 extern lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__1;
 lean_object* l_Lean_Elab_Term_quoteAutoTactic(lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__6;
+extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 lean_object* l_Lean_Elab_Term_elabLetBangDecl___closed__2;
 uint8_t l_Lean_Expr_isAutoParam(lean_object*);
 extern lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__2;
@ -209,6 +205,7 @@ lean_object* l_Lean_Elab_Term_elabBinders___rarg___boxed(lean_object*, lean_obje
 extern lean_object* l_Lean_String_HasQuote___closed__2;
 lean_object* l_Lean_Elab_Term_expandOptType___boxed(lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__25;
 lean_object* l_Lean_Elab_Term_FunBinders_elabFunBindersAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_termElabAttribute;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabLetBangDecl___closed__1;
@ -245,15 +242,17 @@ lean_object* l___private_Lean_Elab_Binders_10__getFunBinderIds_x3f___boxed(lean_
 lean_object* l_Lean_Syntax_getKind(lean_object*);
 lean_object* l___private_Lean_Elab_Binders_4__expandBinderModifier___closed__5;
 lean_object* l_Lean_Elab_Term_elabLetDecl___closed__1;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
 lean_object* l___private_Lean_Elab_Binders_12__checkNoOptAutoParam___closed__3;
 lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 lean_object* l___private_Lean_Elab_Binders_4__expandBinderModifier___closed__6;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__5;
 lean_object* l___private_Lean_Elab_Binders_12__checkNoOptAutoParam___closed__5;
 lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_14__elabFunBinderViews(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Binders_6__matchBinder___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__15;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__3;
 extern lean_object* l_Lean_mkHole___closed__1;
 lean_object* l_Lean_Elab_Term_mkExplicitBinder(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_11__expandFunBindersAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -285,6 +284,7 @@ lean_object* l___private_Lean_Elab_Binders_14__elabFunBinderViews___main___boxed
 lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Term_quoteAutoTactic___main___spec__1___closed__3;
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 uint8_t l_Lean_Expr_isOptParam(lean_object*);
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__7;
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Binders_6__matchBinder___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Elab_Util_1__evalSyntaxConstantUnsafe___closed__1;
 extern lean_object* l_Lean_mkHole___closed__2;
@ -292,7 +292,6 @@ lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lea
 lean_object* l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__9;
 lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__16;
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* l_Lean_Elab_Term_declareTacticSyntax___closed__4;
 lean_object* l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__8;
@ -317,6 +316,7 @@ lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Binders_5__getBind
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Binders_6__matchBinder___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_4__expandBinderModifier___closed__7;
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 lean_object* l___private_Lean_Elab_Binders_1__expandBinderType(lean_object*);
 lean_object* l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__1;
 extern lean_object* l_Lean_mkAppStx___closed__1;
@ -844,7 +844,7 @@ switch (lean_obj_tag(x_1)) {
 case 0:
 {
 lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_4 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
+x_4 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_5 = l_unreachable_x21___rarg(x_4);
 x_6 = lean_apply_2(x_5, x_2, x_3);
 return x_6;
@ -880,12 +880,12 @@ lean_inc(x_17);
 x_18 = lean_ctor_get(x_16, 1);
 lean_inc(x_18);
 lean_dec(x_16);
-x_19 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__6;
+x_19 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__5;
 x_20 = l_Lean_addMacroScope(x_17, x_19, x_14);
 x_21 = lean_box(0);
 x_22 = l_Lean_SourceInfo_inhabited___closed__1;
-x_23 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__4;
-x_24 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__8;
+x_23 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__3;
+x_24 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__7;
 x_25 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_25, 0, x_22);
 lean_ctor_set(x_25, 1, x_23);
@ -926,10 +926,10 @@ if (x_42 == 0)
 {
 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; 
 x_43 = lean_ctor_get(x_41, 0);
-x_44 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__13;
+x_44 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__12;
 x_45 = l_Lean_addMacroScope(x_43, x_44, x_39);
-x_46 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__11;
-x_47 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__16;
+x_46 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__10;
+x_47 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__15;
 x_48 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_48, 0, x_22);
 lean_ctor_set(x_48, 1, x_46);
@ -963,10 +963,10 @@ x_61 = lean_ctor_get(x_41, 1);
 lean_inc(x_61);
 lean_inc(x_60);
 lean_dec(x_41);
-x_62 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__13;
+x_62 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__12;
 x_63 = l_Lean_addMacroScope(x_60, x_62, x_39);
-x_64 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__11;
-x_65 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__16;
+x_64 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__10;
+x_65 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__15;
 x_66 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_66, 0, x_22);
 lean_ctor_set(x_66, 1, x_64);
@ -1036,12 +1036,12 @@ lean_inc(x_87);
 x_88 = lean_ctor_get(x_86, 1);
 lean_inc(x_88);
 lean_dec(x_86);
-x_89 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__6;
+x_89 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__5;
 x_90 = l_Lean_addMacroScope(x_87, x_89, x_84);
 x_91 = lean_box(0);
 x_92 = l_Lean_SourceInfo_inhabited___closed__1;
-x_93 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__4;
-x_94 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__8;
+x_93 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__3;
+x_94 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__7;
 x_95 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_95, 0, x_92);
 lean_ctor_set(x_95, 1, x_93);
@ -1090,10 +1090,10 @@ if (lean_is_exclusive(x_112)) {
 lean_dec_ref(x_112);
 x_115 = lean_box(0);
 }
-x_116 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__13;
+x_116 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__12;
 x_117 = l_Lean_addMacroScope(x_113, x_116, x_110);
-x_118 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__11;
-x_119 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__16;
+x_118 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__10;
+x_119 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__15;
 x_120 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_120, 0, x_92);
 lean_ctor_set(x_120, 1, x_118);
@ -1187,11 +1187,11 @@ if (x_146 == 0)
 {
 lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; 
 x_147 = lean_ctor_get(x_145, 0);
-x_148 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__23;
+x_148 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__22;
 x_149 = l_Lean_addMacroScope(x_147, x_148, x_143);
 x_150 = l_Lean_SourceInfo_inhabited___closed__1;
-x_151 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__22;
-x_152 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__26;
+x_151 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__21;
+x_152 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__25;
 x_153 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_153, 0, x_150);
 lean_ctor_set(x_153, 1, x_151);
@ -1235,11 +1235,11 @@ x_173 = lean_ctor_get(x_145, 1);
 lean_inc(x_173);
 lean_inc(x_172);
 lean_dec(x_145);
-x_174 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__23;
+x_174 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__22;
 x_175 = l_Lean_addMacroScope(x_172, x_174, x_143);
 x_176 = l_Lean_SourceInfo_inhabited___closed__1;
-x_177 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__22;
-x_178 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__26;
+x_177 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__21;
+x_178 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__25;
 x_179 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_179, 0, x_176);
 lean_ctor_set(x_179, 1, x_177);
@ -1304,11 +1304,11 @@ if (lean_is_exclusive(x_203)) {
 lean_dec_ref(x_203);
 x_206 = lean_box(0);
 }
-x_207 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__23;
+x_207 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__22;
 x_208 = l_Lean_addMacroScope(x_204, x_207, x_201);
 x_209 = l_Lean_SourceInfo_inhabited___closed__1;
-x_210 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__22;
-x_211 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__26;
+x_210 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__21;
+x_211 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__25;
 x_212 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_212, 0, x_209);
 lean_ctor_set(x_212, 1, x_210);
@ -5505,7 +5505,7 @@ x_24 = l_Lean_nullKind___closed__2;
 x_25 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_25, 0, x_24);
 lean_ctor_set(x_25, 1, x_23);
-x_26 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_26 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_27 = lean_array_push(x_26, x_25);
 x_28 = l_Lean_Elab_Term_elabArrow___lambda__1___closed__4;
 x_29 = lean_array_push(x_28, x_7);
@ -5515,7 +5515,7 @@ lean_ctor_set(x_30, 1, x_29);
 x_31 = lean_array_push(x_27, x_30);
 x_32 = l___private_Lean_Elab_Term_5__expandCDot___main___closed__4;
 x_33 = lean_array_push(x_31, x_32);
-x_34 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_34 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_35 = lean_array_push(x_33, x_34);
 x_36 = l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
 x_37 = lean_alloc_ctor(1, 2, 0);
@ -5561,7 +5561,7 @@ x_57 = l_Lean_nullKind___closed__2;
 x_58 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_58, 0, x_57);
 lean_ctor_set(x_58, 1, x_56);
-x_59 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_59 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_60 = lean_array_push(x_59, x_58);
 x_61 = l_Lean_Elab_Term_elabArrow___lambda__1___closed__4;
 x_62 = lean_array_push(x_61, x_7);
@ -5571,7 +5571,7 @@ lean_ctor_set(x_63, 1, x_62);
 x_64 = lean_array_push(x_60, x_63);
 x_65 = l___private_Lean_Elab_Term_5__expandCDot___main___closed__4;
 x_66 = lean_array_push(x_64, x_65);
-x_67 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_67 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_68 = lean_array_push(x_66, x_67);
 x_69 = l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
 x_70 = lean_alloc_ctor(1, 2, 0);
--- a/stage0/stdlib/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Lean/Elab/BuiltinNotation.c
@ -188,6 +188,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabAndThen(lean_object*);
 lean_object* l_Lean_Elab_Term_elabseq___closed__1;
 lean_object* l_Lean_Elab_Term_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabTParserMacro(lean_object*);
 extern lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2;
@ -243,6 +244,7 @@ extern lean_object* l_Lean_Parser_Term_div___elambda__1___closed__1;
 lean_object* l___private_Lean_Elab_BuiltinNotation_2__elabTParserMacroAux___closed__4;
 extern lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2;
 lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___closed__20;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__42;
 lean_object* l_Lean_Elab_Term_elabNativeRefl___closed__9;
 extern lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__3;
 extern lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__2;
@ -324,7 +326,6 @@ lean_object* l_Lean_Elab_Term_elabBAnd(lean_object*, lean_object*, lean_object*)
 lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__1;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__41;
 lean_object* l_Lean_Elab_Term_expandSubtype___closed__4;
 extern lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__9;
@ -336,7 +337,6 @@ lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__3;
 extern lean_object* l_Lean_mkAppStx___closed__6;
 lean_object* l_Lean_Elab_Term_elabMap___closed__3;
 lean_object* l_Lean_Elab_Term_elabOr___boxed(lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
 extern lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__1;
 lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___closed__31;
 lean_object* l_Lean_Elab_Term_elabAppend___boxed(lean_object*, lean_object*, lean_object*);
@ -445,7 +445,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___close
 lean_object* l___private_Lean_Elab_BuiltinNotation_5__getPropToDecide___closed__2;
 lean_object* l___private_Lean_Elab_BuiltinNotation_3__mkNativeReflAuxDecl___closed__1;
 extern lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__1;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
 lean_object* l_Lean_Elab_Term_elabGE___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_seqRight___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_expandIf___closed__2;
@ -543,6 +542,7 @@ lean_object* l_Lean_Elab_Term_elabCons(lean_object*, lean_object*, lean_object*)
 lean_object* l___regBuiltin_Lean_Elab_Term_expandIf___closed__1;
 lean_object* l_Lean_Elab_Term_elabMod(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_BuiltinNotation_2__elabTParserMacroAux___closed__10;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__39;
 lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__7;
 extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabPow(lean_object*);
@ -1181,9 +1181,9 @@ x_88 = lean_array_push(x_87, x_69);
 x_89 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_89, 0, x_43);
 lean_ctor_set(x_89, 1, x_88);
-x_90 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_90 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_91 = lean_array_push(x_90, x_89);
-x_92 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_92 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_93 = lean_array_push(x_91, x_92);
 x_94 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_95 = lean_alloc_ctor(1, 2, 0);
@ -1496,9 +1496,9 @@ x_37 = l_Lean_nullKind___closed__2;
 x_38 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_38, 0, x_37);
 lean_ctor_set(x_38, 1, x_36);
-x_39 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_39 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_40 = lean_array_push(x_39, x_38);
-x_41 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_41 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_42 = lean_array_push(x_40, x_41);
 x_43 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_44 = lean_alloc_ctor(1, 2, 0);
@ -1662,9 +1662,9 @@ x_108 = lean_array_push(x_101, x_107);
 x_109 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_109, 0, x_67);
 lean_ctor_set(x_109, 1, x_108);
-x_110 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_110 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_111 = lean_array_push(x_110, x_109);
-x_112 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_112 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_113 = lean_array_push(x_111, x_112);
 x_114 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_115 = lean_alloc_ctor(1, 2, 0);
@ -3705,10 +3705,10 @@ lean_ctor_set(x_74, 0, x_40);
 lean_ctor_set(x_74, 1, x_73);
 x_75 = lean_array_push(x_36, x_74);
 x_76 = lean_array_push(x_36, x_23);
-x_77 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__41;
+x_77 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__40;
 x_78 = l_Lean_addMacroScope(x_57, x_77, x_53);
-x_79 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__40;
-x_80 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
+x_79 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__39;
+x_80 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__42;
 x_81 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_81, 0, x_18);
 lean_ctor_set(x_81, 1, x_79);
@ -3732,9 +3732,9 @@ x_90 = lean_array_push(x_89, x_38);
 x_91 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_91, 0, x_46);
 lean_ctor_set(x_91, 1, x_90);
-x_92 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_92 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_93 = lean_array_push(x_92, x_91);
-x_94 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_94 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_95 = lean_array_push(x_93, x_94);
 x_96 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_97 = lean_alloc_ctor(1, 2, 0);
@ -3795,10 +3795,10 @@ lean_ctor_set(x_121, 0, x_40);
 lean_ctor_set(x_121, 1, x_120);
 x_122 = lean_array_push(x_36, x_121);
 x_123 = lean_array_push(x_36, x_23);
-x_124 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__41;
+x_124 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__40;
 x_125 = l_Lean_addMacroScope(x_103, x_124, x_53);
-x_126 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__40;
-x_127 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
+x_126 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__39;
+x_127 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__42;
 x_128 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_128, 0, x_18);
 lean_ctor_set(x_128, 1, x_126);
@ -3822,9 +3822,9 @@ x_137 = lean_array_push(x_136, x_38);
 x_138 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_138, 0, x_46);
 lean_ctor_set(x_138, 1, x_137);
-x_139 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_139 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_140 = lean_array_push(x_139, x_138);
-x_141 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_141 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_142 = lean_array_push(x_140, x_141);
 x_143 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_144 = lean_alloc_ctor(1, 2, 0);
@ -3923,9 +3923,9 @@ x_189 = lean_array_push(x_188, x_38);
 x_190 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_190, 0, x_46);
 lean_ctor_set(x_190, 1, x_189);
-x_191 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_191 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_192 = lean_array_push(x_191, x_190);
-x_193 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_193 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_194 = lean_array_push(x_192, x_193);
 x_195 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_196 = lean_alloc_ctor(1, 2, 0);
@ -4031,9 +4031,9 @@ x_246 = lean_array_push(x_245, x_38);
 x_247 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_247, 0, x_46);
 lean_ctor_set(x_247, 1, x_246);
-x_248 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_248 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_249 = lean_array_push(x_248, x_247);
-x_250 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_250 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_251 = lean_array_push(x_249, x_250);
 x_252 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_253 = lean_alloc_ctor(1, 2, 0);
--- a/stage0/stdlib/Lean/Elab/Definition.c
+++ b/stage0/stdlib/Lean/Elab/Definition.c
@ -30,7 +30,6 @@ lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__4;
 lean_object* l___private_Lean_Elab_Definition_3__withUsedWhen_x27___rarg___closed__1;
 lean_object* l_Lean_Elab_Command_withDeclId___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
-extern lean_object* l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
 uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Command_6__mkTermContext(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDefVal___closed__2;
@ -73,6 +72,7 @@ lean_object* l___private_Lean_Elab_Definition_3__withUsedWhen_x27___rarg(lean_ob
 lean_object* l_Lean_Elab_Term_collectUsedFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDefLike___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Command_DefKind_isTheorem(uint8_t);
+extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 extern lean_object* l_Lean_NameSet_empty;
 lean_object* l_Lean_Elab_Command_sortDeclLevelParams(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDefVal___closed__3;
@ -877,7 +877,7 @@ lean_dec(x_48);
 lean_dec(x_45);
 lean_dec(x_42);
 lean_dec(x_9);
-x_95 = l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
+x_95 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_96 = l_unreachable_x21___rarg(x_95);
 x_97 = lean_apply_2(x_96, x_12, x_54);
 return x_97;
--- a/stage0/stdlib/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Lean/Elab/Quotation.c
--- a/stage0/stdlib/Lean/Elab/ResolveName.c
+++ b/stage0/stdlib/Lean/Elab/ResolveName.c
@ -892,102 +892,144 @@ lean_inc(x_1);
 x_15 = l___private_Lean_Elab_ResolveName_3__resolveExact(x_1, x_13);
 if (lean_obj_tag(x_15) == 0)
 {
-uint8_t x_16; lean_object* x_17; lean_object* x_18; 
+uint8_t x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; lean_object* x_20; 
 lean_inc(x_1);
 x_16 = l_Lean_Environment_contains(x_1, x_13);
-x_17 = l_Lean_getAliases(x_1, x_13);
+lean_inc(x_13);
+lean_inc(x_1);
+x_17 = l_Lean_mkPrivateName(x_1, x_13);
+lean_inc(x_1);
+x_18 = l_Lean_Environment_contains(x_1, x_17);
+x_19 = l_Lean_getAliases(x_1, x_13);
 if (x_16 == 0)
 {
-lean_object* x_24; lean_object* x_25; 
+if (x_18 == 0)
+{
+lean_object* x_26; lean_object* x_27; 
+lean_dec(x_17);
 lean_inc(x_3);
 lean_inc(x_1);
-x_24 = l___private_Lean_Elab_ResolveName_4__resolveOpenDecls___main(x_1, x_13, x_3, x_14);
-x_25 = l_List_append___rarg(x_17, x_24);
-x_18 = x_25;
-goto block_23;
+x_26 = l___private_Lean_Elab_ResolveName_4__resolveOpenDecls___main(x_1, x_13, x_3, x_14);
+x_27 = l_List_append___rarg(x_19, x_26);
+x_20 = x_27;
+goto block_25;
 }
 else
 {
-lean_object* x_26; lean_object* x_27; lean_object* x_28; 
-lean_inc(x_13);
-x_26 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_26, 0, x_13);
-lean_ctor_set(x_26, 1, x_14);
+lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_17);
+lean_ctor_set(x_28, 1, x_14);
+x_29 = l_List_append___rarg(x_28, x_14);
 lean_inc(x_3);
 lean_inc(x_1);
-x_27 = l___private_Lean_Elab_ResolveName_4__resolveOpenDecls___main(x_1, x_13, x_3, x_26);
-x_28 = l_List_append___rarg(x_17, x_27);
-x_18 = x_28;
-goto block_23;
+x_30 = l___private_Lean_Elab_ResolveName_4__resolveOpenDecls___main(x_1, x_13, x_3, x_29);
+x_31 = l_List_append___rarg(x_19, x_30);
+x_20 = x_31;
+goto block_25;
 }
-block_23:
+}
+else
 {
-if (lean_obj_tag(x_18) == 0)
+lean_object* x_32; 
+lean_inc(x_13);
+x_32 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_32, 0, x_13);
+lean_ctor_set(x_32, 1, x_14);
+if (x_18 == 0)
 {
-lean_object* x_19; 
-x_19 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_19, 0, x_8);
-lean_ctor_set(x_19, 1, x_6);
+lean_object* x_33; lean_object* x_34; 
+lean_dec(x_17);
+lean_inc(x_3);
+lean_inc(x_1);
+x_33 = l___private_Lean_Elab_ResolveName_4__resolveOpenDecls___main(x_1, x_13, x_3, x_32);
+x_34 = l_List_append___rarg(x_19, x_33);
+x_20 = x_34;
+goto block_25;
+}
+else
+{
+lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; 
+x_35 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_35, 0, x_17);
+lean_ctor_set(x_35, 1, x_14);
+x_36 = l_List_append___rarg(x_35, x_32);
+lean_inc(x_3);
+lean_inc(x_1);
+x_37 = l___private_Lean_Elab_ResolveName_4__resolveOpenDecls___main(x_1, x_13, x_3, x_36);
+x_38 = l_List_append___rarg(x_19, x_37);
+x_20 = x_38;
+goto block_25;
+}
+}
+block_25:
+{
+if (lean_obj_tag(x_20) == 0)
+{
+lean_object* x_21; 
+x_21 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_21, 0, x_8);
+lean_ctor_set(x_21, 1, x_6);
 x_5 = x_7;
-x_6 = x_19;
+x_6 = x_21;
 goto _start;
 }
 else
 {
-lean_object* x_21; lean_object* x_22; 
+lean_object* x_23; lean_object* x_24; 
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_3);
 lean_dec(x_1);
-x_21 = l_List_eraseDups___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__1(x_18);
-x_22 = l_List_map___main___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__3(x_6, x_21);
-return x_22;
+x_23 = l_List_eraseDups___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__1(x_20);
+x_24 = l_List_map___main___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__3(x_6, x_23);
+return x_24;
 }
 }
 }
 else
 {
-lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; 
 lean_dec(x_13);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_3);
 lean_dec(x_1);
-x_29 = lean_ctor_get(x_15, 0);
-lean_inc(x_29);
+x_39 = lean_ctor_get(x_15, 0);
+lean_inc(x_39);
 lean_dec(x_15);
-x_30 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_30, 0, x_29);
-lean_ctor_set(x_30, 1, x_6);
-x_31 = lean_box(0);
-x_32 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_32, 0, x_30);
-lean_ctor_set(x_32, 1, x_31);
-return x_32;
+x_40 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_40, 0, x_39);
+lean_ctor_set(x_40, 1, x_6);
+x_41 = lean_box(0);
+x_42 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_42, 0, x_40);
+lean_ctor_set(x_42, 1, x_41);
+return x_42;
 }
 }
 else
 {
-lean_object* x_33; lean_object* x_34; 
+lean_object* x_43; lean_object* x_44; 
 lean_dec(x_13);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_3);
 lean_dec(x_1);
-x_33 = l_List_eraseDups___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__1(x_14);
-x_34 = l_List_map___main___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__4(x_6, x_33);
-return x_34;
+x_43 = l_List_eraseDups___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__1(x_14);
+x_44 = l_List_map___main___at___private_Lean_Elab_ResolveName_5__resolveGlobalNameAux___main___spec__4(x_6, x_43);
+return x_44;
 }
 }
 else
 {
-lean_object* x_35; 
+lean_object* x_45; 
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_1);
-x_35 = lean_box(0);
-return x_35;
+x_45 = lean_box(0);
+return x_45;
 }
 }
 }
--- a/stage0/stdlib/Lean/Elab/StructInst.c
+++ b/stage0/stdlib/Lean/Elab/StructInst.c
@ -180,6 +180,7 @@ lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_toSyntax___boxed(lean_object*,
 lean_object* l___private_Lean_Elab_StructInst_17__groupFields___at___private_Lean_Elab_StructInst_19__expandStruct___main___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_hasFormat(lean_object*);
 extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_23__mkCtorHeader___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_StructInst_Source_isNone___boxed(lean_object*);
 lean_object* l_Lean_Elab_Term_StructInst_Struct_inhabited;
@ -289,12 +290,10 @@ lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_StructInst_3_
 lean_object* l_Lean_Elab_Term_StructInst_findField_x3f(lean_object*, lean_object*);
 extern lean_object* l_Lean_Options_empty;
 lean_object* lean_expr_dbg_to_string(lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
 lean_object* l_Lean_getPathToBaseStructure_x3f(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_modn(size_t, lean_object*);
 extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__2;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
 lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_findDefaultMissing_x3f___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_isRoundDone___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Term_StructInst_findField_x3f___lambda__1(lean_object*, lean_object*);
@ -317,6 +316,7 @@ lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_reduce___main___lambda__2
 lean_object* l_Std_AssocList_find_x3f___main___at___private_Lean_Elab_StructInst_12__mkFieldMap___spec__2(lean_object*, lean_object*);
 uint8_t l_Lean_Expr_isAppOfArity___main(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
+extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1___closed__5;
 lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__18;
 extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10;
@ -393,7 +393,6 @@ extern lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__1;
 lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_Monad___rarg(lean_object*);
 lean_object* lean_panic_fn(lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
 lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_step___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_StructInst_3__isModifyOp_x3f___spec__1___closed__2;
 lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1___closed__4;
@ -534,6 +533,7 @@ lean_object* l___private_Lean_Elab_StructInst_21__getForallBody___main(lean_obje
 lean_object* l_Lean_Elab_Term_StructInst_FieldVal_toSyntax(lean_object*);
 lean_object* l_List_foldlM___main___at___private_Lean_Elab_StructInst_12__mkFieldMap___spec__10___closed__5;
 lean_object* l_Lean_findField_x3f___main(lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 lean_object* l___private_Lean_Elab_StructInst_5__getStructName___closed__1;
 lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefaultAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_StructInst_DefaultFields_reduce___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1341,7 +1341,7 @@ lean_dec(x_5);
 x_17 = lean_ctor_get(x_15, 1);
 lean_inc(x_17);
 lean_dec(x_15);
-x_18 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
+x_18 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_19 = l_unreachable_x21___rarg(x_18);
 x_20 = lean_apply_2(x_19, x_2, x_17);
 return x_20;
@ -2376,12 +2376,12 @@ lean_ctor_set(x_77, 0, x_22);
 lean_ctor_set(x_77, 1, x_76);
 lean_ctor_set(x_77, 2, x_75);
 lean_ctor_set(x_77, 3, x_21);
-x_78 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_78 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_79 = lean_array_push(x_78, x_77);
 x_80 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
 x_81 = lean_array_push(x_79, x_80);
 x_82 = lean_array_push(x_81, x_42);
-x_83 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_83 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_84 = lean_array_push(x_82, x_83);
 x_85 = l_Lean_Parser_Term_namedArgument___elambda__1___closed__2;
 x_86 = lean_alloc_ctor(1, 2, 0);
@ -2606,12 +2606,12 @@ lean_ctor_set(x_214, 0, x_203);
 lean_ctor_set(x_214, 1, x_213);
 lean_ctor_set(x_214, 2, x_212);
 lean_ctor_set(x_214, 3, x_202);
-x_215 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_215 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_216 = lean_array_push(x_215, x_214);
 x_217 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
 x_218 = lean_array_push(x_216, x_217);
 x_219 = lean_array_push(x_218, x_188);
-x_220 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_220 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_221 = lean_array_push(x_219, x_220);
 x_222 = l_Lean_Parser_Term_namedArgument___elambda__1___closed__2;
 x_223 = lean_alloc_ctor(1, 2, 0);
@ -11894,7 +11894,7 @@ lean_dec(x_1);
 x_8 = lean_ctor_get(x_2, 1);
 lean_inc(x_8);
 lean_dec(x_2);
-x_9 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
+x_9 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_10 = l_unreachable_x21___rarg(x_9);
 lean_inc(x_3);
 x_11 = lean_apply_2(x_10, x_3, x_4);
@ -12101,7 +12101,7 @@ lean_dec(x_1);
 x_58 = lean_ctor_get(x_2, 1);
 lean_inc(x_58);
 lean_dec(x_2);
-x_59 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
+x_59 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_60 = l_unreachable_x21___rarg(x_59);
 lean_inc(x_3);
 x_61 = lean_apply_2(x_60, x_3, x_4);
@ -12309,7 +12309,7 @@ lean_dec(x_1);
 x_109 = lean_ctor_get(x_2, 1);
 lean_inc(x_109);
 lean_dec(x_2);
-x_110 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__1;
+x_110 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_111 = l_unreachable_x21___rarg(x_110);
 lean_inc(x_3);
 x_112 = lean_apply_2(x_111, x_3, x_4);
@ -24216,9 +24216,9 @@ x_20 = lean_array_push(x_12, x_19);
 x_21 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_21, 0, x_18);
 lean_ctor_set(x_21, 1, x_20);
-x_22 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_22 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_23 = lean_array_push(x_22, x_21);
-x_24 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_24 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_25 = lean_array_push(x_23, x_24);
 x_26 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_27 = lean_alloc_ctor(1, 2, 0);
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
--- a/stage0/stdlib/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Lean/Elab/Syntax.c
@ -212,6 +212,7 @@ uint8_t l_Lean_Parser_leadingIdentAsSymbol(lean_object*, lean_object*);
 extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__16;
 extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 extern lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__49;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__105;
@ -379,7 +380,6 @@ lean_object* l___private_Lean_Elab_Syntax_6__declareSyntaxCatQuotParser___closed
 extern lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_mkKindName___closed__1;
 lean_object* l___private_Lean_Elab_Syntax_6__declareSyntaxCatQuotParser___closed__26;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__89;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__47;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
@ -538,7 +538,6 @@ lean_object* l_Lean_Elab_Command_elabSyntax___closed__1;
 lean_object* l___private_Lean_Elab_Syntax_9__expandNotationAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_checkLeftRec(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__111;
-extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
 lean_object* l___private_Lean_Elab_Syntax_6__declareSyntaxCatQuotParser___closed__32;
 lean_object* l___private_Lean_Elab_Syntax_6__declareSyntaxCatQuotParser___closed__10;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__97;
@ -723,6 +722,7 @@ extern lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_expandNotationItemIntoSyntaxItem(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__35;
 extern lean_object* l_Lean_Parser_mkAntiquot___closed__2;
+extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 extern lean_object* l_Lean_Elab_Command_liftTermElabM___rarg___closed__1;
 extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__12;
@ -9470,9 +9470,9 @@ x_114 = lean_array_push(x_113, x_23);
 x_115 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_115, 0, x_28);
 lean_ctor_set(x_115, 1, x_114);
-x_116 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
+x_116 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__27;
 x_117 = lean_array_push(x_116, x_115);
-x_118 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_118 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_119 = lean_array_push(x_117, x_118);
 x_120 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_121 = lean_alloc_ctor(1, 2, 0);
@ -12737,7 +12737,7 @@ x_36 = lean_ctor_get(x_34, 0);
 lean_dec(x_36);
 x_37 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_38 = lean_array_push(x_37, x_31);
-x_39 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_39 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_40 = lean_array_push(x_38, x_39);
 x_41 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_42 = lean_alloc_ctor(1, 2, 0);
@ -12756,7 +12756,7 @@ lean_inc(x_45);
 lean_dec(x_34);
 x_46 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_47 = lean_array_push(x_46, x_31);
-x_48 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_48 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_49 = lean_array_push(x_47, x_48);
 x_50 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_51 = lean_alloc_ctor(1, 2, 0);
@ -16142,7 +16142,7 @@ lean_ctor_set(x_47, 1, x_45);
 x_48 = lean_array_push(x_39, x_47);
 x_49 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_50 = lean_array_push(x_49, x_29);
-x_51 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_51 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_52 = lean_array_push(x_50, x_51);
 x_53 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_54 = lean_alloc_ctor(1, 2, 0);
@ -16227,7 +16227,7 @@ lean_ctor_set(x_99, 1, x_97);
 x_100 = lean_array_push(x_79, x_99);
 x_101 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_102 = lean_array_push(x_101, x_29);
-x_103 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_103 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_104 = lean_array_push(x_102, x_103);
 x_105 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_106 = lean_alloc_ctor(1, 2, 0);
@ -16311,7 +16311,7 @@ lean_ctor_set(x_146, 1, x_144);
 x_147 = lean_array_push(x_138, x_146);
 x_148 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_149 = lean_array_push(x_148, x_128);
-x_150 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_150 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_151 = lean_array_push(x_149, x_150);
 x_152 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_153 = lean_alloc_ctor(1, 2, 0);
@ -16398,7 +16398,7 @@ lean_ctor_set(x_199, 1, x_197);
 x_200 = lean_array_push(x_179, x_199);
 x_201 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_202 = lean_array_push(x_201, x_128);
-x_203 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_203 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_204 = lean_array_push(x_202, x_203);
 x_205 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_206 = lean_alloc_ctor(1, 2, 0);
@ -17225,7 +17225,7 @@ lean_ctor_set(x_68, 1, x_66);
 x_69 = lean_array_push(x_48, x_68);
 x_70 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_71 = lean_array_push(x_70, x_42);
-x_72 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_72 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_73 = lean_array_push(x_71, x_72);
 x_74 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_75 = lean_alloc_ctor(1, 2, 0);
@ -17304,7 +17304,7 @@ lean_ctor_set(x_117, 1, x_115);
 x_118 = lean_array_push(x_97, x_117);
 x_119 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_120 = lean_array_push(x_119, x_42);
-x_121 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_121 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_122 = lean_array_push(x_120, x_121);
 x_123 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_124 = lean_alloc_ctor(1, 2, 0);
@ -17399,7 +17399,7 @@ lean_ctor_set(x_171, 1, x_169);
 x_172 = lean_array_push(x_151, x_171);
 x_173 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_174 = lean_array_push(x_173, x_145);
-x_175 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_175 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_176 = lean_array_push(x_174, x_175);
 x_177 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_178 = lean_alloc_ctor(1, 2, 0);
@ -17480,7 +17480,7 @@ lean_ctor_set(x_221, 1, x_219);
 x_222 = lean_array_push(x_201, x_221);
 x_223 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_224 = lean_array_push(x_223, x_145);
-x_225 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_225 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_226 = lean_array_push(x_224, x_225);
 x_227 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_228 = lean_alloc_ctor(1, 2, 0);
@ -18814,7 +18814,7 @@ x_162 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__6
 x_163 = lean_array_push(x_161, x_162);
 x_164 = l_Lean_Elab_Command_expandElab___closed__17;
 x_165 = lean_array_push(x_164, x_47);
-x_166 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_166 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_167 = lean_array_push(x_165, x_166);
 x_168 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_169 = lean_alloc_ctor(1, 2, 0);
@ -19065,7 +19065,7 @@ x_311 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__6
 x_312 = lean_array_push(x_310, x_311);
 x_313 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_314 = lean_array_push(x_313, x_47);
-x_315 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_315 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_316 = lean_array_push(x_314, x_315);
 x_317 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_318 = lean_alloc_ctor(1, 2, 0);
@ -19318,7 +19318,7 @@ x_462 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__6
 x_463 = lean_array_push(x_461, x_462);
 x_464 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_465 = lean_array_push(x_464, x_47);
-x_466 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_466 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_467 = lean_array_push(x_465, x_466);
 x_468 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_469 = lean_alloc_ctor(1, 2, 0);
@ -19614,7 +19614,7 @@ x_629 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__6
 x_630 = lean_array_push(x_628, x_629);
 x_631 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_632 = lean_array_push(x_631, x_47);
-x_633 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_633 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_634 = lean_array_push(x_632, x_633);
 x_635 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_636 = lean_alloc_ctor(1, 2, 0);
@ -19954,7 +19954,7 @@ x_817 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__6
 x_818 = lean_array_push(x_816, x_817);
 x_819 = l_Lean_Elab_Command_expandElab___closed__17;
 x_820 = lean_array_push(x_819, x_702);
-x_821 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_821 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_822 = lean_array_push(x_820, x_821);
 x_823 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_824 = lean_alloc_ctor(1, 2, 0);
@ -20207,7 +20207,7 @@ x_967 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__6
 x_968 = lean_array_push(x_966, x_967);
 x_969 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_970 = lean_array_push(x_969, x_702);
-x_971 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_971 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_972 = lean_array_push(x_970, x_971);
 x_973 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_974 = lean_alloc_ctor(1, 2, 0);
@ -20462,7 +20462,7 @@ x_1119 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__
 x_1120 = lean_array_push(x_1118, x_1119);
 x_1121 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_1122 = lean_array_push(x_1121, x_702);
-x_1123 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_1123 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_1124 = lean_array_push(x_1122, x_1123);
 x_1125 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_1126 = lean_alloc_ctor(1, 2, 0);
@ -20759,7 +20759,7 @@ x_1287 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__
 x_1288 = lean_array_push(x_1286, x_1287);
 x_1289 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__8;
 x_1290 = lean_array_push(x_1289, x_702);
-x_1291 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__44;
+x_1291 = l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
 x_1292 = lean_array_push(x_1290, x_1291);
 x_1293 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
 x_1294 = lean_alloc_ctor(1, 2, 0);
--- a/stage0/stdlib/Lean/Elab/SyntheticMVars.c
+++ b/stage0/stdlib/Lean/Elab/SyntheticMVars.c
@ -35,7 +35,6 @@ lean_object* l_Lean_Elab_Term_liftTacticElabM___rarg(lean_object*, lean_object*,
 lean_object* l___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__10;
 lean_object* l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTermAndSynthesize(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
 uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
 lean_object* l_Lean_fmt___at___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__1(lean_object*);
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
@ -95,7 +94,7 @@ extern lean_object* l___private_Lean_Elab_Util_4__regTraceClasses___closed__1;
 lean_object* l_Lean_Elab_Term_liftTacticElabM(lean_object*);
 lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_inhabited___boxed(lean_object*, lean_object*);
+extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 lean_object* l_Lean_Elab_Term_runTactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_isDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1550,15 +1549,6 @@ x_7 = l___private_Lean_Elab_SyntheticMVars_1__resumeElabTerm(x_1, x_2, x_6, x_4,
 return x_7;
 }
 }
-lean_object* _init_l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_TermElabM_inhabited___boxed), 2, 1);
-lean_closure_set(x_1, 0, lean_box(0));
-return x_1;
-}
-}
 lean_object* l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
@ -1869,7 +1859,7 @@ else
 {
 lean_object* x_32; lean_object* x_33; lean_object* x_34; 
 lean_dec(x_5);
-x_32 = l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
+x_32 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_33 = l_unreachable_x21___rarg(x_32);
 x_34 = lean_apply_2(x_33, x_6, x_9);
 return x_34;
@ -2080,7 +2070,7 @@ lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44;
 x_41 = lean_ctor_get(x_5, 1);
 lean_inc(x_41);
 lean_dec(x_5);
-x_42 = l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
+x_42 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_43 = l_unreachable_x21___rarg(x_42);
 x_44 = lean_apply_2(x_43, x_3, x_41);
 return x_44;
@ -2092,7 +2082,7 @@ lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
 x_45 = lean_ctor_get(x_5, 1);
 lean_inc(x_45);
 lean_dec(x_5);
-x_46 = l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
+x_46 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_47 = l_unreachable_x21___rarg(x_46);
 x_48 = lean_apply_2(x_47, x_3, x_45);
 return x_48;
@ -2176,7 +2166,7 @@ lean_dec(x_3);
 x_17 = lean_ctor_get(x_9, 1);
 lean_inc(x_17);
 lean_dec(x_9);
-x_18 = l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
+x_18 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_19 = l_unreachable_x21___rarg(x_18);
 x_20 = lean_apply_2(x_19, x_7, x_17);
 return x_20;
@ -2192,7 +2182,7 @@ lean_dec(x_3);
 x_21 = lean_ctor_get(x_9, 1);
 lean_inc(x_21);
 lean_dec(x_9);
-x_22 = l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
+x_22 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_23 = l_unreachable_x21___rarg(x_22);
 x_24 = lean_apply_2(x_23, x_7, x_21);
 return x_24;
@ -4113,7 +4103,7 @@ lean_dec(x_6);
 x_36 = lean_ctor_get(x_1, 1);
 lean_inc(x_36);
 lean_dec(x_1);
-x_37 = l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1;
+x_37 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 x_38 = l_unreachable_x21___rarg(x_37);
 lean_inc(x_2);
 x_39 = lean_apply_2(x_38, x_2, x_3);
@ -5870,8 +5860,6 @@ l_Lean_Elab_Term_ensureAssignmentHasNoMVars___closed__2 = _init_l_Lean_Elab_Term
 lean_mark_persistent(l_Lean_Elab_Term_ensureAssignmentHasNoMVars___closed__2);
 l_Lean_Elab_Term_ensureAssignmentHasNoMVars___closed__3 = _init_l_Lean_Elab_Term_ensureAssignmentHasNoMVars___closed__3();
 lean_mark_persistent(l_Lean_Elab_Term_ensureAssignmentHasNoMVars___closed__3);
-l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1 = _init_l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1();
-lean_mark_persistent(l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___closed__1);
 l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___closed__1 = _init_l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___closed__1();
 lean_mark_persistent(l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___closed__1);
 l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__1 = _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__1();
--- a/stage0/stdlib/Lean/Elab/Term.c
+++ b/stage0/stdlib/Lean/Elab/Term.c
@ -60,6 +60,7 @@ lean_object* l___private_Lean_Elab_Term_20__resolveLocalNameAux___main(lean_obje
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__9;
 lean_object* l_Lean_Elab_Term_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Nat_HasQuote___closed__2;
+lean_object* l_unreachable_x21___rarg(lean_object*);
 extern lean_object* l_Lean_nullKind;
 lean_object* l_Lean_Meta_whnfForall(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_monadLog___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
@ -72,6 +73,7 @@ lean_object* l_Lean_Elab_Term_inferType(lean_object*, lean_object*, lean_object*
 lean_object* l_Lean_Elab_Term_mkTermElabAttribute___closed__7;
 lean_object* l_Lean_Elab_Term_assignExprMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_ppGoal___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_hasSorry___main___closed__1;
 lean_object* l_Lean_Elab_Term_elabUsingElabFns___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkTermElabAttribute___closed__3;
@ -375,6 +377,7 @@ lean_object* l_Lean_Elab_Term_tryLiftAndCoe___closed__1;
 lean_object* l_Lean_Elab_Term_TermElabM_inhabited(lean_object*, lean_object*);
 lean_object* l_Std_PersistentArray_foldlM___at___private_Lean_Elab_Term_3__fromMetaState___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkInstMVar(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21(lean_object*, lean_object*, lean_object*);
 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_SMap_empty___at_Lean_Elab_Term_termElabAttribute___spec__1___closed__1;
@ -526,6 +529,7 @@ lean_object* l_Lean_Elab_Term_elabArrayLit___closed__4;
 uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
 lean_object* l_Lean_Elab_Term_TermElabM_inhabited___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkPure(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 lean_object* l_Lean_Elab_Term_mkFreshAnonymousIdent___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabRawNumLit(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_Term_elabUsingElabFns___spec__1(lean_object*, lean_object*);
@ -818,6 +822,7 @@ lean_object* l_Lean_Elab_Term_mkTermElabAttribute___closed__2;
 lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getMCtx___boxed(lean_object*);
 lean_object* l_Lean_Elab_Term_applyResult(lean_object*, lean_object*, lean_object*);
+lean_object* lean_local_ctx_find(lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Term_18__mkPairsAux___main___closed__2;
 lean_object* l_Lean_Meta_isTypeFormer(lean_object*, lean_object*, lean_object*);
@ -1399,6 +1404,90 @@ lean_dec(x_1);
 return x_3;
 }
 }
+lean_object* _init_l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_TermElabM_inhabited___boxed), 2, 1);
+lean_closure_set(x_1, 0, lean_box(0));
+return x_1;
+}
+}
+lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21(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_getLCtx(x_2, 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; 
+x_6 = lean_ctor_get(x_4, 0);
+x_7 = lean_ctor_get(x_4, 1);
+x_8 = l_Lean_Expr_fvarId_x21(x_1);
+x_9 = lean_local_ctx_find(x_6, x_8);
+if (lean_obj_tag(x_9) == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_free_object(x_4);
+x_10 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
+x_11 = l_unreachable_x21___rarg(x_10);
+x_12 = lean_apply_2(x_11, x_2, x_7);
+return x_12;
+}
+else
+{
+lean_object* x_13; 
+lean_dec(x_2);
+x_13 = lean_ctor_get(x_9, 0);
+lean_inc(x_13);
+lean_dec(x_9);
+lean_ctor_set(x_4, 0, x_13);
+return x_4;
+}
+}
+else
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_14 = lean_ctor_get(x_4, 0);
+x_15 = lean_ctor_get(x_4, 1);
+lean_inc(x_15);
+lean_inc(x_14);
+lean_dec(x_4);
+x_16 = l_Lean_Expr_fvarId_x21(x_1);
+x_17 = lean_local_ctx_find(x_14, x_16);
+if (lean_obj_tag(x_17) == 0)
+{
+lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+x_18 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
+x_19 = l_unreachable_x21___rarg(x_18);
+x_20 = lean_apply_2(x_19, x_2, x_15);
+return x_20;
+}
+else
+{
+lean_object* x_21; lean_object* x_22; 
+lean_dec(x_2);
+x_21 = lean_ctor_get(x_17, 0);
+lean_inc(x_21);
+lean_dec(x_17);
+x_22 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_22, 0, x_21);
+lean_ctor_set(x_22, 1, x_15);
+return x_22;
+}
+}
+}
+}
+lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Elab_Term_getFVarLocalDecl_x21(x_1, x_2, x_3);
+lean_dec(x_1);
+return x_4;
+}
+}
 lean_object* l_Lean_Elab_Term_setEnv(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -30885,6 +30974,8 @@ l_Lean_Elab_Term_TermElabResult_inhabited___closed__1 = _init_l_Lean_Elab_Term_T
 lean_mark_persistent(l_Lean_Elab_Term_TermElabResult_inhabited___closed__1);
 l_Lean_Elab_Term_TermElabResult_inhabited = _init_l_Lean_Elab_Term_TermElabResult_inhabited();
 lean_mark_persistent(l_Lean_Elab_Term_TermElabResult_inhabited);
+l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1 = _init_l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1();
+lean_mark_persistent(l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1);
 l_Lean_Elab_Term_monadLog___closed__1 = _init_l_Lean_Elab_Term_monadLog___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__1);
 l_Lean_Elab_Term_monadLog___closed__2 = _init_l_Lean_Elab_Term_monadLog___closed__2();