chore: update stage0

stage0/src/Init/Lean/Elab/StructInst.lean

@@ -14,63 +14,29 @@ namespace Elab
 namespace Term
 namespace StructInst
 
-/- parser! symbol "{" appPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}" -/
-
-namespace ExpandNonAtomicExplicitSource
-
-structure State :=
-(found : Bool := false)
-(source? : Option Syntax := none)
-
-/- Auxiliary function for  `expandNonAtomicExplicitSource` -/
-def main (stx : Syntax) : StateT State TermElabM (Option Syntax) := do
-let args := (stx.getArg 2).getArgs;
-args ← args.mapM $ fun arg =>
-  if arg.getKind == `Lean.Parser.Term.structInstSource then do
-    -- parser! ".." >> optional termParser
-    s ← get;
-    if s.found then
-      liftM $ throwError arg "source has already been specified"
-    else
-      let optSource := arg.getArg 1;
-      if optSource.isNone then do
-        modify $ fun s => { s with found := true };
-        pure arg
-      else do
-        let source := optSource.getArg 0;
-        fvar? ← liftM $ isLocalTermId? source;
-        match fvar? with
-        | some _ => do
-          -- it is already a local variable
-          modify $ fun s => { s with found := true };
-          pure arg
-        | none => do
-          src ← `(src);
-          modify $ fun s => { s with found := true, source? := source };
-          let optSource := optSource.setArg 0 src;
-          let arg := arg.setArg 1 optSource;
-          pure arg
-  else
-    pure arg;
-s ← get;
-match s.source? with
-| none        => pure none
-| some source => do
-  let newStx := stx.setArg 2 (mkNullNode args);
-  `(let src := $source; $newStx)
-
-end ExpandNonAtomicExplicitSource
+/- parser! symbol "{" appPrec >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}" -/
 
 /-
-If `stx` is of the form `{ ... .. s }` and `s` is not a local variable, expand into `let src := s; { ... .. src}`.
+If `stx` is of the form `{ s with ... }` and `s` is not a local variable, expand into `let src := s; { src with ... }`.
 -/
 private def expandNonAtomicExplicitSource (stx : Syntax) : TermElabM (Option Syntax) :=
-withFreshMacroScope $ (ExpandNonAtomicExplicitSource.main stx).run' {}
+withFreshMacroScope $
+  let sourceOpt := stx.getArg 1;
+  if sourceOpt.isNone then pure none  else do
+    let source := sourceOpt.getArg 0;
+    fvar? ← isLocalTermId? source;
+    match fvar? with
+    | some _ => pure none
+    | none   => do
+      src ← `(src);
+      let sourceOpt := sourceOpt.setArg 0 src;
+      let stxNew    := stx.setArg 1 sourceOpt;
+      `(let src := $source; $stxNew)
 
 inductive Source
 | none     -- structure instance source has not been provieded
 | implicit (stx : Syntax) -- `..`
-| explicit (stx : Syntax) (src : Expr) -- `.. term`
+| explicit (stx : Syntax) (src : Expr) -- `src with`
 
 instance Source.inhabited : Inhabited Source := ⟨Source.none⟩
 
@@ -78,35 +44,25 @@ def Source.isNone : Source → Bool
 | Source.none => true
 | _           => false
 
-instance Source.hasFormat : HasFormat Source :=
-⟨fun src => match src with
- | Source.none           => ""
- | Source.implicit _     => " .."
- | Source.explicit _ src => " .. " ++ format src⟩
-
-def Source.addSyntax : Source → Array Syntax → Array Syntax
-| Source.none,           acc => acc
-| Source.implicit stx,   acc => acc.push stx
-| Source.explicit stx _, acc => acc.push stx
+def setStructSourceSyntax (structStx : Syntax) : Source → Syntax
+| Source.none           => (structStx.setArg 1 mkNullNode).setArg 3 mkNullNode
+| Source.implicit stx   => (structStx.setArg 1 mkNullNode).setArg 3 stx
+| Source.explicit stx _ => (structStx.setArg 1 stx).setArg 3 mkNullNode
 
 private def getStructSource (stx : Syntax) : TermElabM Source :=
-let args := (stx.getArg 2).getArgs;
-args.foldSepByM
-  (fun arg r =>
-    if arg.getKind == `Lean.Parser.Term.structInstSource then
-      -- parser! ".." >> optional termParser
-      if !r.isNone then throwError arg "source has already been specified"
-      else
-        let optTerm := arg.getArg 1;
-        if optTerm.isNone then pure $ Source.implicit arg
-        else do
-          fvar? ← isLocalTermId? (optTerm.getArg 0);
-          match fvar? with
-          | none      => unreachable! -- expandNonAtomicExplicitSource must have been used when we get here
-          | some fvar => pure $ Source.explicit arg fvar
-    else
-      pure r)
-  Source.none
+let explicitSource := stx.getArg 1;
+let implicitSource := stx.getArg 3;
+if explicitSource.isNone && implicitSource.isNone then
+  pure Source.none
+else if explicitSource.isNone then
+  pure $ Source.implicit implicitSource
+else if implicitSource.isNone then do
+  fvar? ← isLocalTermId? (explicitSource.getArg 0);
+  match fvar? with
+  | none      => unreachable! -- expandNonAtomicExplicitSource must have been used when we get here
+  | some src  => pure $ Source.explicit explicitSource src
+else
+  throwError stx "invalid structure instance `with` and `..` cannot be used together"
 
 /-
   We say a `{ ... }` notation is a `modifyOp` if it contains only one
@@ -117,34 +73,29 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
 let args := (stx.getArg 2).getArgs;
 s? ← args.foldSepByM
   (fun arg s? =>
-    let k := arg.getKind;
-    if k == `Lean.Parser.Term.structInstSource then pure s?
-    else if k == `Lean.Parser.Term.structInstField then
-      /- Remark: the syntax for `structInstField` is
-         ```
-         def structInstLVal   := (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
-         def structInstField  := parser! structInstLVal >> " := " >> termParser
-         ``` -/
-      let lval := arg.getArg 0;
-      let k    := lval.getKind;
-      if k == `Lean.Parser.Term.structInstArrayRef then
-        match s? with
-        | none   => pure (some arg)
-        | some s =>
-          if s.getKind == `Lean.Parser.Term.structInstArrayRef then
-            throwError arg "invalid {...} notation, at most one `[..]` at a given level"
-          else
-            throwError arg "invalid {...} notation, can't mix field and `[..]` at a given level"
-      else
-        match s? with
-        | none   => pure (some arg)
-        | some s =>
-          if s.getKind == `Lean.Parser.Term.structInstArrayRef then
-            throwError arg "invalid {...} notation, can't mix field and `[..]` at a given level"
-          else
-            pure s?
+    /- Remark: the syntax for `structInstField` is
+       ```
+       def structInstLVal   := (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
+       def structInstField  := parser! structInstLVal >> " := " >> termParser
+       ``` -/
+    let lval := arg.getArg 0;
+    let k    := lval.getKind;
+    if k == `Lean.Parser.Term.structInstArrayRef then
+      match s? with
+      | none   => pure (some arg)
+      | some s =>
+        if s.getKind == `Lean.Parser.Term.structInstArrayRef then
+          throwError arg "invalid {...} notation, at most one `[..]` at a given level"
+        else
+          throwError arg "invalid {...} notation, can't mix field and `[..]` at a given level"
     else
-      throwError arg "unexpected {...} notation")
+      match s? with
+      | none   => pure (some arg)
+      | some s =>
+        if s.getKind == `Lean.Parser.Term.structInstArrayRef then
+          throwError arg "invalid {...} notation, can't mix field and `[..]` at a given level"
+        else
+          pure s?)
   none;
 match s? with
 | none   => pure none
@@ -154,10 +105,12 @@ private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option
 let continue (val : Syntax) : TermElabM Expr := do {
   let lval := modifyOp.getArg 0;
   let idx  := lval.getArg 1;
-  let self := (source.getArg 1).getArg 0;
+  let self := source.getArg 0;
   stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val));
+  trace `Elab.struct.modifyOp stx $ fun _ => stx ++ "\n===>\n" ++ stxNew;
   withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-};
+}; do
+trace `Elab.struct.modifyOp stx $ fun _ => modifyOp ++ "\nSource: " ++ source;
 let rest := modifyOp.getArg 1;
 if rest.isNone then do
   continue (modifyOp.getArg 3)
@@ -169,43 +122,33 @@ else do
   let valRest   := mkNullNode (restArgs.extract 1 restArgs.size);
   let valField  := modifyOp.setArg 0 valFirst;
   let valField  := valField.setArg 1 valRest;
-  let valSource := source.modifyArg 1 $ fun stx => stx.modifyArg 0 $ fun _ => s;
-  let val       := stx.setArg 1 mkNullNode;
-  let val       := val.setArg 2 $ mkNullNode #[valField, mkAtomFrom stx ", ", valSource];
+  let valSource := source.modifyArg 0 $ fun _ => s;
+  let val       := stx.setArg 1 valSource;
+  let val       := val.setArg 2 $ mkNullNode #[valField];
+  trace `Elab.struct.modifyOp stx $ fun _ => stx ++ "\nval: " ++ val;
   continue val
 
-/- Get structure name and elaborate explicit source (if avialable) -/
-private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name :=
-let arg := stx.getArg 1;
-if !arg.isNone then do
-  r : List (Name × List String) ← resolveGlobalName (arg.getIdAt 0);
-  env ← getEnv;
-  let r := r.filter $ fun p => p.2.isEmpty && isStructureLike env p.1;
-  let candidates := r.map $ fun p => p.1;
-  match candidates with
-  | [c] => pure c
-  | []  => throwError arg "invalid {...} notation, structure expected"
-  | _   => throwError arg ("invalid {...} notation, ambiguous " ++ toString candidates)
-else do
-  let ref := stx;
-  tryPostponeIfNoneOrMVar expectedType?;
-  let useSource : Unit → TermElabM Name := fun _ =>
-    match sourceView with
-    | Source.explicit _ src => do
-      srcType ← inferType stx src;
-      srcType ← whnf stx srcType;
-      tryPostponeIfMVar srcType;
-      match srcType.getAppFn with
-      | Expr.const constName _ _ => pure constName
-      | _ => throwError stx ("invalid {...} notation, source type is not of the form (C ...)" ++ indentExpr srcType)
-    | _ => throwError ref ("invalid {...} notation, expected type is not of the form (C ...)" ++ indentExpr expectedType?.get!);
-  match expectedType? with
-  | none => useSource ()
-  | some expectedType => do
-    expectedType ← whnf ref expectedType;
-    match expectedType.getAppFn with
+/- Get structure name and elaborate explicit source (if available) -/
+private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
+let ref := stx;
+tryPostponeIfNoneOrMVar expectedType?;
+let useSource : Unit → TermElabM Name := fun _ =>
+  match sourceView with
+  | Source.explicit _ src => do
+    srcType ← inferType stx src;
+    srcType ← whnf stx srcType;
+    tryPostponeIfMVar srcType;
+    match srcType.getAppFn with
     | Expr.const constName _ _ => pure constName
-    | _                        => useSource ()
+    | _ => throwError stx ("invalid {...} notation, source type is not of the form (C ...)" ++ indentExpr srcType)
+  | _ => throwError ref ("invalid {...} notation, expected type is not of the form (C ...)" ++ indentExpr expectedType?.get!);
+match expectedType? with
+| none => useSource ()
+| some expectedType => do
+  expectedType ← whnf ref expectedType;
+  match expectedType.getAppFn with
+  | Expr.const constName _ _ => pure constName
+  | _                        => useSource ()
 
 inductive FieldLHS
 | fieldName  (ref : Syntax) (name : Name)
@@ -261,7 +204,11 @@ Format.joinSep field.lhs " . " ++ " := " ++
 
 partial def formatStruct : Struct → Format
 | ⟨_, structName, fields, source⟩ =>
-  "{" ++ fmt structName ++ " . " ++ Format.joinSep (fields.map (formatField formatStruct)) ", " ++ fmt source ++ "}"
+  let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", ";
+  match source with
+  | Source.none           => "{" ++ fieldsFmt ++ "}"
+  | Source.implicit _     => "{" ++ fieldsFmt ++ " .. }"
+  | Source.explicit _ src => "{" ++ format src ++ " with " ++ fieldsFmt ++ "}"
 
 instance Struct.hasFormat : HasFormat Struct     := ⟨formatStruct⟩
 instance Struct.hasToString : HasToString Struct := ⟨toString ∘ format⟩
@@ -358,11 +305,11 @@ s.modifyFieldsM $ fun fields => do
    This method expands parent structure fields using the path to the parent structure.
    For example,
    ```
-   { C . x := 0, y := 0, z := true }
+   { x := 0, y := 0, z := true : C }
    ```
    is expanded into
    ```
-   { C . toB.toA.x := 0, toB.y := 0, z := true }
+   { toB.toA.x := 0, toB.y := 0, z := true : C }
    ``` -/
 private def expandParentFields (s : Struct) : TermElabM Struct := do
 env ← getEnv;
@@ -414,7 +361,7 @@ private def mkSubstructSource (ref : Syntax) (structName : Name) (fieldNames : A
 match src with
 | Source.explicit stx src => do
   idx ← getFieldIdx ref structName fieldNames fieldName;
-  let stx := stx.modifyArg 1 $ fun stx => stx.modifyArg 0 $ fun stx => mkProjStx stx fieldName;
+  let stx := stx.modifyArg 0 $ fun stx => mkProjStx stx fieldName;
   pure $ Source.explicit stx (mkProj structName idx src)
 | s => pure s
 
@@ -438,10 +385,10 @@ s.modifyFieldsM $ fun fields => do
       | none => do
         -- It is not a substructure field. Thus, we wrap fields using `Syntax`, and use `elabTerm` to process them.
         let valStx := s.ref; -- construct substructure syntax using s.ref as template
-        let valStx := valStx.setArg 1 mkNullNode; -- erase optional struct name
+        let valStx := valStx.setArg 4 mkNullNode; -- erase optional expected type
         let args   := substructFields.toArray.map $ Field.toSyntax;
-        let args   := substructSource.addSyntax args;
         let valStx := valStx.setArg 2 (mkSepStx args (mkAtomFrom s.ref ","));
+        let valStx := setStructSourceSyntax valStx substructSource;
         pure { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
 
 def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
@@ -473,8 +420,8 @@ fields ← fieldNames.foldlM
         | Source.none           => addField FieldVal.default
         | Source.implicit _     => addField (FieldVal.term (mkHole s.ref))
         | Source.explicit stx _ =>
-          -- stx is of the form `".." >> optional termParser`
-          let src := (stx.getArg 1).getArg 0;
+          -- stx is of the form `optional (try (termParser >> "with"))`
+          let src := (stx.getArg 0).getArg 0;
           let val := mkProjStx src fieldName;
           addField (FieldVal.term val))
   [];
@@ -818,18 +765,34 @@ match mkStructView stx structName source with
   DefaultFields.propagate struct;
   pure r
 
+private def expandStructInstExpectedType (stx : Syntax) : MacroM (Option Syntax) :=
+let expectedArg := stx.getArg 4;
+if expectedArg.isNone then pure none
+else
+  let expected := expectedArg.getArg 1;
+  let stxNew   := stx.setArg 4 mkNullNode;
+  `(($stxNew : $expected))
+
 @[builtinTermElab structInst] def elabStructInst : TermElab :=
 fun stx expectedType? => do
-  stxNew? ← expandNonAtomicExplicitSource stx;
+  stxNew? ← liftMacroM $ expandStructInstExpectedType stx;
   match stxNew? with
   | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-  | none => do
-    sourceView ← getStructSource stx;
-    modifyOp?  ← isModifyOp? stx;
-    match modifyOp?, sourceView with
-    | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
-    | some _,        _                        => throwError stx ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
-    | _,             _                        => elabStructInstAux stx expectedType? sourceView
+  | none        => do
+    stxNew? ← expandNonAtomicExplicitSource stx;
+    match stxNew? with
+    | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+    | none => do
+      sourceView ← getStructSource stx;
+      modifyOp?  ← isModifyOp? stx;
+      match modifyOp?, sourceView with
+      | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
+      | some _,        _                        => throwError stx ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
+      | _,             _                        => elabStructInstAux stx expectedType? sourceView
+
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Elab.struct;
+pure ()
 
 end StructInst
 end Term

stage0/stdlib/Init/Lean/Elab/Binders.c

@@ -20,7 +20,9 @@ lean_object* l_Lean_Elab_Term_elabBinders(lean_object*);
 lean_object* l_Lean_Elab_Term_mkForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Binders_12__checkNoOptAutoParam___closed__4;
 lean_object* l___private_Init_Lean_Elab_Binders_2__expandBinderIdent___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__12;
 extern lean_object* l___private_Init_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10;
+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_Array_umapMAux___main___at___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
@@ -747,11 +749,9 @@ lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_SourceInfo_inhabited___closed__1;
-x_2 = l_PersistentHashMap_Stats_toString___closed__5;
-x_3 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_3, 0, x_1);
-lean_ctor_set(x_3, 1, x_2);
+x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__4;
+x_2 = l___private_Init_Lean_Elab_Term_5__expandCDot___main___closed__4;
+x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
 }
@@ -759,8 +759,8 @@ lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__4;
-x_2 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_2 = l___private_Init_Lean_Elab_Term_5__expandCDot___main___closed__4;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -769,9 +769,9 @@ lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_structInst___elambda__1___closed__2;
-x_2 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__6;
-x_3 = lean_alloc_ctor(1, 2, 0);
+x_1 = l_Lean_SourceInfo_inhabited___closed__1;
+x_2 = l_PersistentHashMap_Stats_toString___closed__5;
+x_3 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
 return x_3;
@@ -781,7 +781,7 @@ lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Array_empty___closed__1;
+x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__6;
 x_2 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
@@ -790,26 +790,48 @@ return x_3;
 lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__9() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("invalic auto tactic, identifier is not allowed");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Term_structInst___elambda__1___closed__2;
+x_2 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__8;
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
 }
 }
 lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__10() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__9;
-x_2 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Array_empty___closed__1;
+x_2 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__9;
+x_3 = lean_array_push(x_1, x_2);
+return x_3;
 }
 }
 lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__11() {
 _start:
 {
+lean_object* x_1; 
+x_1 = lean_mk_string("invalic auto tactic, identifier is not allowed");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__12() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__10;
+x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__11;
+x_2 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__13() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__12;
 x_2 = lean_alloc_ctor(0, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@@ -1191,7 +1213,7 @@ x_163 = l_Lean_String_HasQuote___closed__2;
 x_164 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_164, 0, x_163);
 lean_ctor_set(x_164, 1, x_162);
-x_165 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__8;
+x_165 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__10;
 x_166 = lean_array_push(x_165, x_164);
 x_167 = l_Lean_nullKind___closed__2;
 x_168 = lean_alloc_ctor(1, 2, 0);
@@ -1239,7 +1261,7 @@ x_189 = l_Lean_String_HasQuote___closed__2;
 x_190 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_190, 0, x_189);
 lean_ctor_set(x_190, 1, x_188);
-x_191 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__8;
+x_191 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__10;
 x_192 = lean_array_push(x_191, x_190);
 x_193 = l_Lean_nullKind___closed__2;
 x_194 = lean_alloc_ctor(1, 2, 0);
@@ -1308,7 +1330,7 @@ x_223 = l_Lean_String_HasQuote___closed__2;
 x_224 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_224, 0, x_223);
 lean_ctor_set(x_224, 1, x_222);
-x_225 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__8;
+x_225 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__10;
 x_226 = lean_array_push(x_225, x_224);
 x_227 = l_Lean_nullKind___closed__2;
 x_228 = lean_alloc_ctor(1, 2, 0);
@@ -1332,7 +1354,7 @@ return x_232;
 default: 
 {
 lean_object* x_233; lean_object* x_234; 
-x_233 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__11;
+x_233 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__13;
 x_234 = l_Lean_Elab_Term_throwError___rarg(x_1, x_233, x_2, x_3);
 lean_dec(x_1);
 return x_234;
@@ -25249,6 +25271,10 @@ l_Lean_Elab_Term_quoteAutoTactic___main___closed__10 = _init_l_Lean_Elab_Term_qu
 lean_mark_persistent(l_Lean_Elab_Term_quoteAutoTactic___main___closed__10);
 l_Lean_Elab_Term_quoteAutoTactic___main___closed__11 = _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__11();
 lean_mark_persistent(l_Lean_Elab_Term_quoteAutoTactic___main___closed__11);
+l_Lean_Elab_Term_quoteAutoTactic___main___closed__12 = _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__12();
+lean_mark_persistent(l_Lean_Elab_Term_quoteAutoTactic___main___closed__12);
+l_Lean_Elab_Term_quoteAutoTactic___main___closed__13 = _init_l_Lean_Elab_Term_quoteAutoTactic___main___closed__13();
+lean_mark_persistent(l_Lean_Elab_Term_quoteAutoTactic___main___closed__13);
 l_Lean_Elab_Term_declareTacticSyntax___closed__1 = _init_l_Lean_Elab_Term_declareTacticSyntax___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_declareTacticSyntax___closed__1);
 l_Lean_Elab_Term_declareTacticSyntax___closed__2 = _init_l_Lean_Elab_Term_declareTacticSyntax___closed__2();

stage0/stdlib/Init/Lean/Elab/DoNotation.c

@@ -132,6 +132,7 @@ extern lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 extern lean_object* l___private_Init_Lean_Elab_Quotation_8__letBindRhss___main___closed__11;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabDo(lean_object*);
 lean_object* l___private_Init_Lean_Elab_DoNotation_2__extractBind(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_DoNotation_11__processDoElemsAux___main___closed__3;
 lean_object* l___private_Init_Lean_Elab_DoNotation_5__expandLiftMethodAux___main___closed__2;
@@ -169,7 +170,6 @@ lean_object* l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___boxed(l
 lean_object* l___private_Init_Lean_Elab_DoNotation_1__mkIdBindFor___closed__4;
 extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__6;
 lean_object* l___private_Init_Lean_Elab_DoNotation_4__hasLiftMethod___main___boxed(lean_object*);
-extern lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_Elab_DoNotation_4__hasLiftMethod___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
@@ -2184,7 +2184,7 @@ lean_ctor_set(x_43, 0, x_42);
 lean_ctor_set(x_43, 1, x_41);
 x_44 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_45 = lean_array_push(x_44, x_43);
-x_46 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_46 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_47 = lean_array_push(x_45, x_46);
 x_48 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_49 = lean_alloc_ctor(1, 2, 0);
@@ -2371,7 +2371,7 @@ lean_ctor_set(x_132, 0, x_131);
 lean_ctor_set(x_132, 1, x_130);
 x_133 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_134 = lean_array_push(x_133, x_132);
-x_135 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_135 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_136 = lean_array_push(x_134, x_135);
 x_137 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_138 = lean_alloc_ctor(1, 2, 0);
@@ -2779,7 +2779,7 @@ lean_ctor_set(x_375, 0, x_374);
 lean_ctor_set(x_375, 1, x_373);
 x_376 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_377 = lean_array_push(x_376, x_375);
-x_378 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_378 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_379 = lean_array_push(x_377, x_378);
 x_380 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_381 = lean_alloc_ctor(1, 2, 0);
@@ -2885,7 +2885,7 @@ lean_ctor_set(x_430, 0, x_429);
 lean_ctor_set(x_430, 1, x_428);
 x_431 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_432 = lean_array_push(x_431, x_430);
-x_433 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_433 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_434 = lean_array_push(x_432, x_433);
 x_435 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_436 = lean_alloc_ctor(1, 2, 0);
@@ -3065,7 +3065,7 @@ lean_ctor_set(x_514, 0, x_513);
 lean_ctor_set(x_514, 1, x_512);
 x_515 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_516 = lean_array_push(x_515, x_514);
-x_517 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_517 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_518 = lean_array_push(x_516, x_517);
 x_519 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_520 = lean_alloc_ctor(1, 2, 0);
@@ -3473,7 +3473,7 @@ lean_ctor_set(x_757, 0, x_756);
 lean_ctor_set(x_757, 1, x_755);
 x_758 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_759 = lean_array_push(x_758, x_757);
-x_760 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_760 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_761 = lean_array_push(x_759, x_760);
 x_762 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_763 = lean_alloc_ctor(1, 2, 0);
@@ -3583,7 +3583,7 @@ lean_ctor_set(x_814, 0, x_813);
 lean_ctor_set(x_814, 1, x_812);
 x_815 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_816 = lean_array_push(x_815, x_814);
-x_817 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_817 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_818 = lean_array_push(x_816, x_817);
 x_819 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_820 = lean_alloc_ctor(1, 2, 0);
@@ -3701,7 +3701,7 @@ lean_ctor_set(x_19, 0, x_18);
 lean_ctor_set(x_19, 1, x_17);
 x_20 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__2;
 x_21 = lean_array_push(x_20, x_19);
-x_22 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__5;
+x_22 = l_Lean_Elab_Term_quoteAutoTactic___main___closed__7;
 x_23 = lean_array_push(x_21, x_22);
 x_24 = l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
 x_25 = lean_alloc_ctor(1, 2, 0);