chore: update stage0

stage0/src/Init/Data/Array/Basic.lean

@@ -474,6 +474,9 @@ variable {β : Type u}
 @[inline] def modify [Inhabited α] (a : Array α) (i : Nat) (f : α → α) : Array α :=
 Id.run $ a.modifyM i f
 
+@[inline] def modifyOp [Inhabited α] (self : Array α) (idx : Nat) (f : α → α) : Array α :=
+self.modify idx f
+
 @[inline] def mapIdx (f : Nat → α → β) (a : Array α) : Array β :=
 Id.run $ mapIdxM f a
 

stage0/src/Init/Lean/Elab.lean

@@ -19,3 +19,4 @@ import Init.Lean.Elab.Tactic
 import Init.Lean.Elab.Syntax
 import Init.Lean.Elab.Match
 import Init.Lean.Elab.DoNotation
+import Init.Lean.Elab.StructInst

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

@@ -558,10 +558,24 @@ fun stx => do
   | Syntax.atom _ "false" => setOption ref optionName (DataValue.ofBool false)
   | _ => logError val ("unexpected set_option value " ++ toString val)
 
+/-
+  `declId` is of the form
+  ```
+  parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
+  ```
+  but we also accept a single identifier to users to make macro writing more convenient .
+-/
+def expandDeclId (declId : Syntax) : Name × Syntax :=
+if declId.isIdent then
+  (declId.getId, mkNullNode)
+else
+  let id             := declId.getIdAt 0;
+  let optUnivDeclStx := declId.getArg 1;
+  (id, optUnivDeclStx)
+
 @[inline] def withDeclId (declId : Syntax) (f : Name → CommandElabM Unit) : CommandElabM Unit := do
 -- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
-let id             := declId.getIdAt 0;
-let optUnivDeclStx := declId.getArg 1;
+let (id, optUnivDeclStx) := expandDeclId declId;
 savedLevelNames ← getLevelNames;
 levelNames      ←
   if optUnivDeclStx.isNone then

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

@@ -12,25 +12,30 @@ namespace Lean
 namespace Elab
 namespace Term
 
-private def mkIdBindFor (ref : Syntax) (type : Expr) : TermElabM (Expr × Expr) := do
+structure ExtractMonadResult :=
+(m           : Expr)
+(α           : Expr)
+(hasBindInst : Expr)
+
+private def mkIdBindFor (ref : Syntax) (type : Expr) : TermElabM ExtractMonadResult := do
 u ← getLevel ref type;
 let id        := Lean.mkConst `Id [u];
 let idBindVal := Lean.mkConst `Id.hasBind [u];
-pure (id, idBindVal)
+pure { m := id, hasBindInst := idBindVal, α := type }
 
-private def extractMonad (ref : Syntax) (expectedType? : Option Expr) : TermElabM (Expr × Expr) := do
+private def extractMonad (ref : Syntax) (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
 match expectedType? with
 | none => throwError ref "invalid do notation, expected type is not available"
 | some expectedType => do
   type ← withReducible $ whnf ref expectedType;
   when type.getAppFn.isMVar $ throwError ref "invalid do notation, expected type is not available";
   match type with
-  | Expr.app m _ _ =>
+  | Expr.app m α _ =>
     catch
       (do
         bindInstType ← mkAppM ref `HasBind #[m];
         bindInstVal  ← synthesizeInst ref bindInstType;
-        pure (m, bindInstVal))
+        pure { m := m, hasBindInst := bindInstVal, α := α })
       (fun ex => mkIdBindFor ref type)
   | _ => mkIdBindFor ref type
 
@@ -137,9 +142,51 @@ private partial def expandDoElemsAux : Bool → Array Syntax → Nat → MacroM
 private partial def expandDoElems (doElems : Array Syntax) : MacroM (Option Syntax) :=
 expandDoElemsAux false doElems 0
 
+private def extractTypeFormerAppArg (ref : Syntax) (type : Expr) : TermElabM Expr := do
+type ← withReducible $ whnf ref type;
+match type with
+| Expr.app _ a _ => pure a
+| _              => throwError ref ("type former application expected" ++ indentExpr type)
+
+/-
+We try to coerce first using `HasMonadLift` because it is more flexible than coercions.
+Recall that type class resolution never assigns metavariables created by other modules.
+Now, consider the following scenario
+```lean
+def g (x : Nat) : IO Nat := ...
+deg h (x : Nat) : StateT Nat IO Nat := do
+v ← g x;
+IO.Println v;
+...
+```
+Let's assume there is no other occurrence of `v` in `h`.
+Thus, we have that the expected of `g x` is `StateT Nat IO ?α`,
+and the given type is `IO Nat`. So, even if we add a coercion.
+```
+instance {α m n} [HasLiftT m n] {α} : Coe (m α) (n α) := ...
+```
+It is not applicable because TC would have to assign `?α := Nat`.
+On the other hand, TC can easily solve `[HasLiftT IO (StateT Nat IO)]`
+since this goal does not contain any metavariables. And then, we
+convert `g x` into `liftM $ g x`.
+-/
+private def mkMonadLift (ref : Syntax) (expectedMonad : Expr) (expectedType : Expr) (val : Expr) (valType : Expr) : TermElabM Expr := do
+-- liftM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : HasMonadLiftT m n] {α : Type u_1}, m α → n α
+extractResult    ← extractMonad ref valType;
+hasMonadLiftType ← mkAppM ref `HasMonadLiftT #[extractResult.m, expectedMonad];
+hasMonadLiftVal  ← synthesizeInst ref hasMonadLiftType;
+u_1 ← getDecLevel ref extractResult.α;
+u_2 ← getDecLevel ref valType;
+u_3 ← getDecLevel ref expectedType;
+let newVal := mkAppN (Lean.mkConst `liftM [u_1, u_2, u_3]) #[extractResult.m, expectedMonad, hasMonadLiftVal, extractResult.α, val];
+ensureHasType ref expectedType newVal
+
 private def ensureDoElemType (ref : Syntax) (expectedMonad : Expr) (expectedType : Expr) (val : Expr) : TermElabM Expr := do
--- TODO: try MonadLift
-ensureHasType ref expectedType val
+valType ← inferType ref val;
+condM (isDefEq ref valType expectedType) (pure val) $
+  catch
+    (mkMonadLift ref expectedMonad expectedType val valType)
+    (fun _ => ensureHasType ref expectedType val)
 
 structure ProcessedDoElem :=
 (action : Expr)
@@ -147,12 +194,6 @@ structure ProcessedDoElem :=
 
 instance ProcessedDoElem.inhabited : Inhabited ProcessedDoElem := ⟨⟨arbitrary _, arbitrary _⟩⟩
 
-private def extractTypeFormerAppArg (ref : Syntax) (type : Expr) : TermElabM Expr := do
-type ← withReducible $ whnf ref type;
-match type with
-| Expr.app _ a _ => pure a
-| _              => throwError ref ("type former application expected" ++ indentExpr type)
-
 /-
 HasBind.bind : ∀ {m : Type u_1 → Type u_2} [self : HasBind m] {α β : Type u_1}, m α → (α → m β) → m β
 -/
@@ -162,11 +203,9 @@ if elems.isEmpty then
 else do
   let x := elems.back.var; -- any variable would work since they must be in the same universe
   xType ← inferType ref x;
-  u_1 ← getLevel ref xType;
-  u_1 ← decLevel ref u_1;
+  u_1 ← getDecLevel ref xType;
   bodyType ← inferType ref body;
-  u_2 ← getLevel ref bodyType;
-  u_2 ← decLevel ref u_2;
+  u_2 ← getDecLevel ref bodyType;
   let bindAndInst := mkApp2 (Lean.mkConst `HasBind.bind [u_1, u_2]) m bindInstVal;
   elems.foldrM
     (fun elem body => do
@@ -224,7 +263,7 @@ fun stx expectedType? => do
   | none => do
     trace `Elab.do ref $ fun _ => stx;
     let doElems := doElems.getSepElems;
-    (m, bindInstVal) ← extractMonad ref expectedType?;
+    { m := m, hasBindInst := bindInstVal, .. } ← extractMonad ref expectedType?;
     result ← processDoElems doElems m bindInstVal expectedType?.get!;
     -- dbgTrace ("result: " ++ toString result);
     pure result

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

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Elab.Term
+import Init.Lean.Elab.TermBinders
+import Init.Lean.Elab.Quotation
+
+namespace Lean
+namespace Elab
+namespace Term
+
+
+end Term
+end Elab
+end Lean

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

@@ -294,6 +294,13 @@ match u? with
 | some u => pure u
 | none   => throwError ref ("invalid universe level, " ++ u ++ " is not greater than 0")
 
+/- This function is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`.
+   Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level,
+   and then decrement 1 to obtain `u`. -/
+def getDecLevel (ref : Syntax) (type : Expr) : TermElabM Level := do
+u ← getLevel ref type;
+decLevel ref u
+
 def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
 fun ctx s =>
   match (x { .. ctx }).run { .. s } with
@@ -378,7 +385,7 @@ private partial def hasCDot : Syntax → Bool
   The extra state `Array Syntax` contains the new binder names.
   If `stx` is a `·`, we create a fresh identifier, store in the
   extra state, and return it. Otherwise, we just return `stx`. -/
-private partial def expandCDot : Syntax → StateT (Array Syntax) TermElabM Syntax
+private partial def expandCDot : Syntax → StateT (Array Syntax) MacroM Syntax
 | stx@(Syntax.node k args) =>
   if k == `Lean.Parser.Term.paren then pure stx
   else if k == `Lean.Parser.Term.cdot then withFreshMacroScope $ do
@@ -396,7 +403,7 @@ private partial def expandCDot : Syntax → StateT (Array Syntax) TermElabM Synt
   Examples:
   - `· + 1` => `fun _a_1 => _a_1 + 1`
   - `f · · b` => `fun _a_1 _a_2 => f _a_1 _a_2 b` -/
-def expandCDot? (stx : Syntax) : TermElabM (Option Syntax) :=
+def expandCDot? (stx : Syntax) : MacroM (Option Syntax) :=
 if hasCDot stx then do
   (newStx, binders) ← (expandCDot stx).run #[];
   `(fun $binders* => $newStx)
@@ -721,7 +728,7 @@ fun stx expectedType? =>
   | none => throwError stx ("invalid tactic block, expected type has not been provided")
 
 /-- Main loop for `mkPairs`. -/
-private partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → TermElabM Syntax
+private partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → MacroM Syntax
 | i, acc =>
   if i > 0 then do
     let i    := i - 1;
@@ -732,7 +739,7 @@ private partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → TermE
     pure acc
 
 /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
-def mkPairs (elems : Array Syntax) : TermElabM Syntax :=
+def mkPairs (elems : Array Syntax) : MacroM Syntax :=
 mkPairsAux elems (elems.size - 1) elems.back
 
 /--
@@ -745,7 +752,7 @@ mkPairsAux elems (elems.size - 1) elems.back
   - `(· + ·)`
   - `(f · a b)` -/
 private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
-stx? ← expandCDot? stx;
+stx? ← liftMacroM $ expandCDot? stx;
 match stx? with
 | some stx' => withMacroExpansion stx stx' (elabTerm stx' expectedType?)
 | none      => elabTerm stx expectedType?
@@ -761,7 +768,7 @@ fun stx expectedType? =>
     ensureHasType ref type e
   | `(($e))         => elabCDot e expectedType?
   | `(($e, $es*))   => do
-    pairs ← mkPairs (#[e] ++ es.getEvenElems);
+    pairs ← liftMacroM $ mkPairs (#[e] ++ es.getEvenElems);
     withMacroExpansion stx pairs (elabTerm pairs expectedType?)
   | _ => throwError stx "unexpected parentheses notation"
 

stage0/src/Init/Lean/Meta/ExprDefEq.lean

@@ -185,6 +185,16 @@ private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr →
 lctx ← getLCtx;
 isDefEqBindingAux lctx #[] a b #[]
 
+private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
+traceCtx `Meta.isDefEq.assign.checkTypes $ do
+  -- must check whether types are definitionally equal or not, before assigning and returning true
+  mvarType ← inferType mvar;
+  vType    ← inferType v;
+  condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
+    (do assignExprMVar mvar.mvarId! v; pure true)
+    (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
+        pure false)
+
 /-
   Each metavariable is declared in a particular local context.
   We use the notation `C |- ?m : t` to denote a metavariable `?m` that
@@ -337,12 +347,10 @@ isDefEqBindingAux lctx #[] a b #[]
 
 namespace CheckAssignment
 
-structure Context :=
-(lctx         : LocalContext)
+structure Context extends Meta.Context :=
 (mvarId       : MVarId)
 (mvarDecl     : MetavarDecl)
 (fvars        : Array Expr)
-(ctxApprox    : Bool)
 (hasCtxLocals : Bool)
 
 inductive Exception
@@ -351,23 +359,27 @@ inductive Exception
 | outOfScopeFVar                     (fvarId : FVarId)
 | readOnlyMVarWithBiggerLCtx         (mvarId : MVarId)
 | unknownExprMVar                    (mvarId : MVarId)
+| meta (ex : Meta.Exception)
 
-structure State :=
-(mctx  : MetavarContext)
-(ngen  : NameGenerator)
-(cache : ExprStructMap Expr := {})
+structure State extends Meta.State :=
+(checkCache : ExprStructMap Expr := {})
 
 abbrev CheckAssignmentM := ReaderT Context (EStateM Exception State)
 
 private def findCached? (e : Expr) : CheckAssignmentM (Option Expr) := do
-s ← get; pure $ s.cache.find? e
+s ← get; pure $ s.checkCache.find? e
 
 private def cache (e r : Expr) : CheckAssignmentM Unit :=
-modify $ fun s => { cache := s.cache.insert e r, .. s }
+modify $ fun s => { checkCache := s.checkCache.insert e r, .. s }
 
 instance : MonadCache Expr Expr CheckAssignmentM :=
 { findCached? := findCached?, cache := cache }
 
+def liftMetaM {α} (x : MetaM α) : CheckAssignmentM α :=
+fun ctx s => match x ctx.toContext s.toState with
+  | EStateM.Result.ok a newS     => EStateM.Result.ok a { toState := newS, .. s }
+  | EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { toState := newS, .. s }
+
 @[inline] private def visit (f : Expr → CheckAssignmentM Expr) (e : Expr) : CheckAssignmentM Expr :=
 if !e.hasExprMVar && !e.hasFVar then pure e else checkCache e f
 
@@ -395,31 +407,41 @@ pure (mkMVar mvarId)
 let mvarId := mvar.mvarId!;
 ctx  ← read;
 mctx ← getMCtx;
-match mctx.getExprAssignment? mvarId with
-| some v => visit check v
-| none   =>
-  if mvarId == ctx.mvarId then throw Exception.occursCheck
-  else match mctx.findDecl? mvarId with
-    | none          => throw $ Exception.unknownExprMVar mvarId
-    | some mvarDecl =>
-      if ctx.hasCtxLocals then throw $ Exception.useFOApprox -- we use option c) described at workaround A2
-      else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx then pure mvar
-      else if mvarDecl.depth != mctx.depth || mvarDecl.kind.isSyntheticOpaque then throw $ Exception.readOnlyMVarWithBiggerLCtx mvarId
-      else if ctx.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx then do
-        mvarType ← check mvarDecl.type;
-        /- Create an auxiliary metavariable with a smaller context and "checked" type.
-           Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains
-           a metavariable that we also need to reduce the context. -/
-        newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
-        modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
-        pure newMVar
-      else
-        pure mvar
+if mvarId == ctx.mvarId then throw Exception.occursCheck
+else match mctx.findDecl? mvarId with
+  | none          => throw $ Exception.unknownExprMVar mvarId
+  | some mvarDecl =>
+    if ctx.hasCtxLocals then throw $ Exception.useFOApprox -- we use option c) described at workaround A2
+    else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx then pure mvar
+    else if mvarDecl.depth != mctx.depth || mvarDecl.kind.isSyntheticOpaque then throw $ Exception.readOnlyMVarWithBiggerLCtx mvarId
+    else if ctx.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx then do
+      mvarType ← check mvarDecl.type;
+      /- Create an auxiliary metavariable with a smaller context and "checked" type.
+         Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains
+         a metavariable that we also need to reduce the context. -/
+      newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
+      modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
+      pure newMVar
+    else
+      pure mvar
+
+/-
+  Auxiliary function used to "fix" subterms of the form `?m x_1 ... x_n` where `x_i`s are free variables,
+  and one of them is out-of-scope.
+  See `Expr.app` case at `check`.
+  If `ctxApprox` is true, then we solve this case by creating a fresh metavariable ?n with the correct scope,
+  an assigning `?m := fun _ ... _ => ?n` -/
+def assignToConstFun (mvar : Expr) (numArgs : Nat) (newMVar : Expr) : MetaM Bool := do
+mvarType ← inferType mvar;
+forallBoundedTelescope mvarType numArgs $ fun xs _ =>
+  if xs.size != numArgs then pure false
+  else do
+    v ← mkLambda xs newMVar;
+    checkTypesAndAssign mvar v
 
 partial def check : Expr → CheckAssignmentM Expr
 | e@(Expr.mdata _ b _)     => do b ← visit check b; pure $ e.updateMData! b
 | e@(Expr.proj _ _ s _)    => do s ← visit check s; pure $ e.updateProj! s
-| e@(Expr.app f a _)       => do f ← visit check f; a ← visit check a; pure $ e.updateApp! f a
 | e@(Expr.lam _ d b _)     => do d ← visit check d; b ← visit check b; pure $ e.updateLambdaE! d b
 | e@(Expr.forallE _ d b _) => do d ← visit check d; b ← visit check b; pure $ e.updateForallE! d b
 | e@(Expr.letE _ t v b _)  => do t ← visit check t; v ← visit check v; b ← visit check b; pure $ e.updateLet! t v b
@@ -430,6 +452,29 @@ partial def check : Expr → CheckAssignmentM Expr
 | e@(Expr.fvar _ _)        => visit (checkFVar check) e
 | e@(Expr.mvar _ _)        => visit (checkMVar check) e
 | Expr.localE _ _ _ _      => unreachable!
+| e@(Expr.app _ _ _)       => e.withApp $ fun f args => do
+  ctx ← read;
+  if f.isMVar && ctx.config.ctxApprox && args.all Expr.isFVar then do
+    f ← visit (checkMVar check) f;
+    catch
+      (do
+        args ← args.mapM (visit check);
+        pure $ mkAppN f args)
+      (fun ex => match ex with
+        | Exception.outOfScopeFVar _ => do
+          eType ← liftMetaM $ inferType e;
+          mvarType ← check eType;
+          /- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar`
+            Note that `mvarType` may be different from `eType`. -/
+          newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
+          condM (liftMetaM $ assignToConstFun f args.size newMVar)
+            (pure newMVar)
+            (throw ex)
+        | _ => throw ex)
+  else do
+    f ← visit check f;
+    args ← args.mapM (visit check);
+    pure $ mkAppN f args
 
 end CheckAssignment
 
@@ -449,6 +494,7 @@ match ex with
 | CheckAssignment.Exception.unknownExprMVar mvarId =>
   -- This case can only happen if the MetaM API is being misused
   throwEx $ Exception.unknownExprMVar mvarId
+| CheckAssignment.Exception.meta ex => throw ex
 
 namespace CheckAssignmentQuick
 
@@ -492,6 +538,20 @@ partial def check
 
 end CheckAssignmentQuick
 
+-- See checkAssignment
+def checkAssignmentAux (mvarId : MVarId) (mvarDecl : MetavarDecl) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : MetaM (Option Expr) :=
+fun ctx s =>
+  let checkCtx : CheckAssignment.Context := {
+    mvarId       := mvarId,
+    mvarDecl     := s.mctx.getDecl mvarId,
+    fvars        := fvars,
+    hasCtxLocals := hasCtxLocals,
+    toContext    := ctx
+  };
+  match (CheckAssignment.check v checkCtx).run { toState := s } with
+  | EStateM.Result.ok e newS     => EStateM.Result.ok (some e) newS.toState
+  | EStateM.Result.error ex newS => checkAssignmentFailure mvarId fvars v ex ctx newS.toState
+
 /--
   Auxiliary function for handling constraints of the form `?m a₁ ... aₙ =?= v`.
   It will check whether we can perform the assignment
@@ -501,24 +561,19 @@ end CheckAssignmentQuick
   The result is `none` if the assignment can't be performed.
   The result is `some newV` where `newV` is a possibly updated `v`. This method may need
   to unfold let-declarations. -/
-def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) :=
-fun ctx s => if !v.hasExprMVar && !v.hasFVar then EStateM.Result.ok (some v) s else
-  let mvarDecl     := s.mctx.getDecl mvarId;
+def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) := do
+if !v.hasExprMVar && !v.hasFVar then
+  pure (some v)
+else do
+  mvarDecl ← getMVarDecl mvarId;
   let hasCtxLocals := fvars.any $ fun fvar => mvarDecl.lctx.containsFVar fvar;
-  if CheckAssignmentQuick.check hasCtxLocals ctx.config.ctxApprox s.mctx ctx.lctx mvarDecl mvarId fvars v then
-    EStateM.Result.ok (some v) s
-  else
-    let checkCtx : CheckAssignment.Context := {
-      lctx         := ctx.lctx,
-      mvarId       := mvarId,
-      mvarDecl     := s.mctx.getDecl mvarId,
-      fvars        := fvars,
-      ctxApprox    := ctx.config.ctxApprox,
-      hasCtxLocals := hasCtxLocals
-    };
-    match (CheckAssignment.check v checkCtx).run { mctx := s.mctx, ngen := s.ngen } with
-    | EStateM.Result.ok e newS     => EStateM.Result.ok (some e) { mctx := newS.mctx, ngen := newS.ngen, .. s }
-    | EStateM.Result.error ex newS => checkAssignmentFailure mvarId fvars v ex ctx { ngen := newS.ngen, .. s }
+  ctx ← read;
+  mctx ← getMCtx;
+  if CheckAssignmentQuick.check hasCtxLocals ctx.config.ctxApprox mctx ctx.lctx mvarDecl mvarId fvars v then
+    pure (some v)
+  else do
+    v ← instantiateMVars v;
+    checkAssignmentAux mvarId mvarDecl fvars hasCtxLocals v
 
 /-
   We try to unify arguments before we try to unify the functions.
@@ -623,16 +678,6 @@ private def simpAssignmentArg (arg : Expr) : MetaM Expr := do
 arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg;
 simpAssignmentArgAux arg
 
-private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
-traceCtx `Meta.isDefEq.assign.checkTypes $ do
-  -- must check whether types are definitionally equal or not, before assigning and returning true
-  mvarType ← inferType mvar;
-  vType    ← inferType v;
-  condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
-    (do assignExprMVar mvar.mvarId! v; pure true)
-    (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
-        pure false)
-
 private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
 let mvarId := mvar.mvarId!;
 v? ← checkAssignment mvarId #[] v;
@@ -653,13 +698,18 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
     let arg := args.get ⟨i, h⟩;
     arg ← simpAssignmentArg arg;
     let args := args.set ⟨i, h⟩ arg;
-    let useFOApprox : Unit → MetaM Bool := fun _ =>
-      if cfg.foApprox && v.isApp then
-        processAssignmentFOApprox mvar args v
-      else if cfg.constApprox then
+    let useConstApprox : Unit → MetaM Bool := fun _ =>
+      if cfg.constApprox then
         processConstApprox mvar args.size v
       else
         pure false;
+    let useFOApprox : Unit → MetaM Bool := fun _ =>
+      if cfg.foApprox && v.isApp then
+        condM (processAssignmentFOApprox mvar args v)
+          (pure true)
+          (useConstApprox ())
+      else
+        useConstApprox ();
     match arg with
     | Expr.fvar fvarId _ =>
       if args.anyRange 0 i (fun prevArg => prevArg == arg) then

stage0/src/Init/Lean/Parser/Term.lean

@@ -58,7 +58,9 @@ def haveAssign := parser! " := " >> termParser
 @[builtinTermParser] def «suffices» := parser! "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
 @[builtinTermParser] def «show»     := parser! "show " >> termParser >> fromTerm
 @[builtinTermParser] def «fun»      := parser! unicodeSymbol "λ" "fun" >> many1 (termParser appPrec) >> darrow >> termParser
-def structInstField  := parser! ident >> " := " >> termParser
+def structInstArrayRef := parser! "[" >> termParser >>"]"
+def structInstLVal   := (ident <|> structInstArrayRef) >> many (("." >> ident) <|> structInstArrayRef)
+def structInstField  := parser! structInstLVal >> " := " >> termParser
 def structInstSource := parser! ".." >> optional termParser
 @[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}"
 def typeSpec := parser! " : " >> termParser

stage0/stdlib/Init/Data/Array/Basic.c

@@ -94,6 +94,7 @@ lean_object* l___private_Init_Data_Array_Basic_1__swapAtPanic_x21___rarg___close
 lean_object* l_Array_insertAtAux___main(lean_object*);
 lean_object* l_Array_iterateM_u2082Aux___main___at_Array_foldlM_u2082___spec__1(lean_object*, lean_object*);
 lean_object* l_Array_empty___closed__1;
+lean_object* l_Array_modifyOp(lean_object*);
 lean_object* l___private_Init_Data_Array_Basic_4__foldrRangeMAux___main___at_Array_foldrRange___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_modifyM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_eraseIdxSzAuxInstance___rarg(lean_object*);
@@ -391,6 +392,7 @@ lean_object* l_Array_getD___rarg___boxed(lean_object*, lean_object*, lean_object
 lean_object* l___private_Init_Data_Array_Basic_4__foldrRangeMAux___main___at_Array_foldrRange___spec__1(lean_object*, lean_object*);
 lean_object* l_Array_findSomeRevMAux___main___at_Array_findSomeRev_x21___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldrRangeM(lean_object*, lean_object*);
+lean_object* l_Array_modifyOp___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlStepM___boxed(lean_object*, lean_object*);
 lean_object* l_Array_foldrRange___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_findRevMAux___main___at_Array_findRev_x3f___spec__1(lean_object*);
@@ -486,6 +488,7 @@ lean_object* l_Array_eraseIdx_x27___rarg(lean_object*, lean_object*);
 lean_object* l_Array_findIdx_x21(lean_object*);
 lean_object* l_Array_back___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_filterMAux___boxed(lean_object*);
+lean_object* l_Array_modifyOp___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main(lean_object*);
 lean_object* l_Array_indexOf___rarg(lean_object*, lean_object*, lean_object*);
@@ -6686,6 +6689,47 @@ lean_dec(x_3);
 return x_5;
 }
 }
+lean_object* l_Array_modifyOp___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; uint8_t x_6; 
+x_5 = lean_array_get_size(x_2);
+x_6 = lean_nat_dec_lt(x_3, x_5);
+lean_dec(x_5);
+if (x_6 == 0)
+{
+lean_dec(x_4);
+lean_dec(x_1);
+return x_2;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+x_7 = lean_array_fget(x_2, x_3);
+x_8 = lean_array_fset(x_2, x_3, x_1);
+x_9 = lean_apply_1(x_4, x_7);
+x_10 = lean_array_fset(x_8, x_3, x_9);
+return x_10;
+}
+}
+}
+lean_object* l_Array_modifyOp(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Array_modifyOp___rarg___boxed), 4, 0);
+return x_2;
+}
+}
+lean_object* l_Array_modifyOp___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Array_modifyOp___rarg(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
 lean_object* l_Array_umapMAux___main___at_Array_mapIdx___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -8349,7 +8393,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Data_Array_Basic_1__swapAtPanic_x21___rarg___closed__3;
-x_2 = lean_unsigned_to_nat(669u);
+x_2 = lean_unsigned_to_nat(672u);
 x_3 = lean_unsigned_to_nat(20u);
 x_4 = l_Array_insertAt___rarg___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);

stage0/stdlib/Init/Lean/Elab.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab
-// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration Init.Lean.Elab.Tactic Init.Lean.Elab.Syntax Init.Lean.Elab.Match Init.Lean.Elab.DoNotation
+// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration Init.Lean.Elab.Tactic Init.Lean.Elab.Syntax Init.Lean.Elab.Match Init.Lean.Elab.DoNotation Init.Lean.Elab.StructInst
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -28,6 +28,7 @@ lean_object* initialize_Init_Lean_Elab_Tactic(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Syntax(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Match(lean_object*);
 lean_object* initialize_Init_Lean_Elab_DoNotation(lean_object*);
+lean_object* initialize_Init_Lean_Elab_StructInst(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab(lean_object* w) {
 lean_object * res;
@@ -78,6 +79,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_DoNotation(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_StructInst(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

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

@@ -0,0 +1,37 @@
+// Lean compiler output
+// Module: Init.Lean.Elab.StructInst
+// Imports: Init.Lean.Elab.Term Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation
+#include "runtime/lean.h"
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* initialize_Init_Lean_Elab_Term(lean_object*);
+lean_object* initialize_Init_Lean_Elab_TermBinders(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Quotation(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_Lean_Elab_StructInst(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_mk_io_result(lean_box(0));
+_G_initialized = true;
+res = initialize_Init_Lean_Elab_Term(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_TermBinders(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Quotation(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_mk_io_result(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif

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

@@ -31,6 +31,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabFun___closed__1;
 lean_object* l___private_Init_Lean_Elab_TermBinders_10__expandFunBindersAux___main___closed__3;
 extern lean_object* l_Lean_List_format___rarg___closed__2;
 uint8_t lean_name_eq(lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Meta_ExprDefEq_7__checkTypesAndAssign___closed__8;
 lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
 lean_object* lean_local_ctx_mk_let_decl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabBinder___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -51,7 +52,6 @@ uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_TermBinders_8__getFunBinderIdsAux_x3f(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_TermBinders_5__matchBinder___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_TermBinders_10__expandFunBindersAux___main___closed__2;
-extern lean_object* l___private_Init_Lean_Meta_ExprDefEq_17__checkTypesAndAssign___closed__5;
 lean_object* l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___closed__4;
 lean_object* l___private_Init_Lean_Elab_TermBinders_9__getFunBinderIds_x3f(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
@@ -118,6 +118,7 @@ lean_object* l_Lean_Elab_Term_elabFun___boxed(lean_object*, lean_object*, lean_o
 lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__3;
 lean_object* l_Lean_Elab_Term_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Meta_ExprDefEq_7__checkTypesAndAssign___closed__7;
 lean_object* l___private_Init_Lean_Elab_TermBinders_6__elabBinderViews___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
@@ -242,7 +243,6 @@ extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed_
 lean_object* l_Lean_Elab_Term_elabForall(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_TermBinders_3__expandOptIdent___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrow(lean_object*);
-extern lean_object* l___private_Init_Lean_Meta_ExprDefEq_10__checkAssignmentFailure___closed__5;
 lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__3;
 extern lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__1;
@@ -18386,7 +18386,7 @@ lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean
 lean_inc(x_2);
 x_23 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_23, 0, x_2);
-x_24 = l___private_Init_Lean_Meta_ExprDefEq_17__checkTypesAndAssign___closed__5;
+x_24 = l___private_Init_Lean_Meta_ExprDefEq_7__checkTypesAndAssign___closed__7;
 x_25 = lean_alloc_ctor(9, 2, 0);
 lean_ctor_set(x_25, 0, x_23);
 lean_ctor_set(x_25, 1, x_24);
@@ -18396,7 +18396,7 @@ lean_ctor_set(x_26, 0, x_14);
 x_27 = lean_alloc_ctor(9, 2, 0);
 lean_ctor_set(x_27, 0, x_25);
 lean_ctor_set(x_27, 1, x_26);
-x_28 = l___private_Init_Lean_Meta_ExprDefEq_10__checkAssignmentFailure___closed__5;
+x_28 = l___private_Init_Lean_Meta_ExprDefEq_7__checkTypesAndAssign___closed__8;
 x_29 = lean_alloc_ctor(9, 2, 0);
 lean_ctor_set(x_29, 0, x_27);
 lean_ctor_set(x_29, 1, x_28);

stage0/stdlib/Init/Lean/Parser/Command.c

@@ -240,7 +240,6 @@ lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Command_attributes___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_init__quot___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__1;
-extern lean_object* l_Lean_Parser_Term_listLit___closed__4;
 lean_object* l_Lean_Parser_Command_section___elambda__1___closed__8;
 lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*);
 lean_object* l_Lean_Parser_Command_declModifiers___closed__13;
@@ -250,7 +249,6 @@ lean_object* l_Lean_Parser_Command_commentBody___closed__1;
 lean_object* l_Lean_Parser_Command_attribute___closed__12;
 lean_object* l_Lean_Parser_Command_export___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_extends;
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_init__quot___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_abbrev___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__13;
@@ -474,6 +472,7 @@ lean_object* l_Lean_Parser_Command_namespace___elambda__1(lean_object*, lean_obj
 lean_object* l_Lean_Parser_Command_section___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_attrArg;
 lean_object* l_Lean_Parser_Command_variables___closed__4;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__1;
 lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__15;
 lean_object* l_Lean_Parser_Command_openSimple___closed__3;
@@ -688,7 +687,6 @@ lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__5;
 extern lean_object* l_Lean_Parser_Term_letIdLhs___closed__1;
 lean_object* l_Lean_Parser_Command_init__quot___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Term_optType___elambda__1(lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Term_stxQuot___closed__3;
 lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Command_declValEqns___elambda__1___closed__1;
@@ -748,6 +746,7 @@ lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__4;
 extern lean_object* l_Lean_Parser_numLit;
 lean_object* l_Lean_Parser_Command_noncomputable___closed__1;
 lean_object* l_Lean_Parser_Command_openRenamingItem___closed__5;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__2;
 lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__5;
@@ -763,7 +762,6 @@ lean_object* l_Lean_Parser_numLit___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_abbrev___closed__1;
 lean_object* l_Lean_Parser_Command_open___closed__1;
 lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__1;
-extern lean_object* l_Lean_Parser_Term_instBinder___closed__1;
 lean_object* l_Lean_Parser_Command_structImplicitBinder;
 lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_set__option___closed__8;
@@ -790,11 +788,11 @@ lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__13;
 lean_object* l_Lean_Parser_Command_axiom___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_structCtor___closed__5;
 extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_private___closed__4;
 lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__5;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_private___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_declModifiers___elambda__1(lean_object*, lean_object*);
@@ -889,6 +887,7 @@ lean_object* l_Lean_Parser_Command_openOnly___closed__2;
 extern lean_object* l_Lean_Parser_unicodeSymbolFn___closed__1;
 lean_object* l_Lean_Parser_Term_stxQuot___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_structureTk___elambda__1___closed__4;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_section___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__4;
@@ -1031,6 +1030,7 @@ lean_object* l_Lean_Parser_Term_stxQuot___closed__1;
 lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Command_attrArg___closed__3;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Command_export___elambda__1___closed__6;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_structExplicitBinder___elambda__1___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_def___closed__4;
@@ -1095,6 +1095,7 @@ lean_object* l_Lean_Parser_Command_declId___closed__6;
 lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__7;
 lean_object* l_Lean_Parser_Command_universe;
 lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__9;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Command_resolve__name___closed__4;
 lean_object* l_Lean_Parser_Command_structInstBinder___closed__7;
 lean_object* l_Lean_Parser_Term_stxQuot___closed__4;
@@ -1134,7 +1135,6 @@ lean_object* l_Lean_Parser_Command_declValEqns;
 lean_object* l_Lean_Parser_Command_declModifiers___closed__9;
 lean_object* l_Lean_Parser_Command_declaration___closed__14;
 lean_object* l_Lean_Parser_Command_example___closed__1;
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__6;
 extern lean_object* l_Lean_Parser_Level_paren___closed__1;
 lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__3;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_synth(lean_object*);
@@ -3125,13 +3125,13 @@ lean_object* x_26; lean_object* x_27; uint8_t x_28;
 x_26 = lean_ctor_get(x_25, 1);
 lean_inc(x_26);
 lean_dec(x_25);
-x_27 = l_Lean_Parser_Term_listLit___elambda__1___closed__6;
+x_27 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6;
 x_28 = lean_string_dec_eq(x_26, x_27);
 lean_dec(x_26);
 if (x_28 == 0)
 {
 lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_29 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_29 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_29, x_21);
 x_31 = l_Lean_Parser_Command_attributes___elambda__1___closed__2;
 x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_15);
@@ -3154,7 +3154,7 @@ else
 {
 lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; 
 lean_dec(x_25);
-x_37 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_37 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_38 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_37, x_21);
 x_39 = l_Lean_Parser_Command_attributes___elambda__1___closed__2;
 x_40 = l_Lean_Parser_ParserState_mkNode(x_38, x_39, x_15);
@@ -3167,7 +3167,7 @@ else
 {
 lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; 
 lean_dec(x_23);
-x_42 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_42 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_43 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_42, x_21);
 x_44 = l_Lean_Parser_Command_attributes___elambda__1___closed__2;
 x_45 = l_Lean_Parser_ParserState_mkNode(x_43, x_44, x_15);
@@ -3231,7 +3231,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Command_attributes___closed__2;
-x_2 = l_Lean_Parser_Term_listLit___closed__4;
+x_2 = l_Lean_Parser_Term_structInstArrayRef___closed__2;
 x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;
 }
@@ -12872,13 +12872,13 @@ lean_object* x_83; lean_object* x_84; uint8_t x_85;
 x_83 = lean_ctor_get(x_82, 1);
 lean_inc(x_83);
 lean_dec(x_82);
-x_84 = l_Lean_Parser_Term_listLit___elambda__1___closed__5;
+x_84 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5;
 x_85 = lean_string_dec_eq(x_83, x_84);
 lean_dec(x_83);
 if (x_85 == 0)
 {
 lean_object* x_86; lean_object* x_87; 
-x_86 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_86 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_inc(x_7);
 x_87 = l_Lean_Parser_ParserState_mkErrorsAt(x_79, x_86, x_7);
 x_53 = x_87;
@@ -12894,7 +12894,7 @@ else
 {
 lean_object* x_88; lean_object* x_89; 
 lean_dec(x_82);
-x_88 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_88 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_inc(x_7);
 x_89 = l_Lean_Parser_ParserState_mkErrorsAt(x_79, x_88, x_7);
 x_53 = x_89;
@@ -12905,7 +12905,7 @@ else
 {
 lean_object* x_90; lean_object* x_91; 
 lean_dec(x_80);
-x_90 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_90 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_inc(x_7);
 x_91 = l_Lean_Parser_ParserState_mkErrorsAt(x_79, x_90, x_7);
 x_53 = x_91;
@@ -12944,13 +12944,13 @@ lean_object* x_25; lean_object* x_26; uint8_t x_27;
 x_25 = lean_ctor_get(x_24, 1);
 lean_inc(x_25);
 lean_dec(x_24);
-x_26 = l_Lean_Parser_Term_listLit___elambda__1___closed__6;
+x_26 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6;
 x_27 = lean_string_dec_eq(x_25, x_26);
 lean_dec(x_25);
 if (x_27 == 0)
 {
 lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_28 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_28 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_21, x_28, x_20);
 x_30 = l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2;
 x_31 = l_Lean_Parser_ParserState_mkNode(x_29, x_30, x_15);
@@ -12973,7 +12973,7 @@ else
 {
 lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; 
 lean_dec(x_24);
-x_36 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_36 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_37 = l_Lean_Parser_ParserState_mkErrorsAt(x_21, x_36, x_20);
 x_38 = l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2;
 x_39 = l_Lean_Parser_ParserState_mkNode(x_37, x_38, x_15);
@@ -12986,7 +12986,7 @@ else
 {
 lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; 
 lean_dec(x_22);
-x_41 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_41 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_42 = l_Lean_Parser_ParserState_mkErrorsAt(x_21, x_41, x_20);
 x_43 = l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2;
 x_44 = l_Lean_Parser_ParserState_mkNode(x_42, x_43, x_15);
@@ -13119,7 +13119,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Command_optDeclSig;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_listLit___closed__4;
+x_3 = l_Lean_Parser_Term_structInstArrayRef___closed__2;
 x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
 return x_4;
 }
@@ -13148,7 +13148,7 @@ lean_object* _init_l_Lean_Parser_Command_structInstBinder___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_instBinder___closed__1;
+x_1 = l_Lean_Parser_Term_structInstArrayRef___closed__1;
 x_2 = l_Lean_Parser_Command_structInstBinder___closed__3;
 x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;
@@ -20961,13 +20961,13 @@ lean_object* x_47; lean_object* x_48; uint8_t x_49;
 x_47 = lean_ctor_get(x_46, 1);
 lean_inc(x_47);
 lean_dec(x_46);
-x_48 = l_Lean_Parser_Term_listLit___elambda__1___closed__6;
+x_48 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6;
 x_49 = lean_string_dec_eq(x_47, x_48);
 lean_dec(x_47);
 if (x_49 == 0)
 {
 lean_object* x_50; lean_object* x_51; 
-x_50 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_50 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_50, x_42);
 x_16 = x_51;
 goto block_36;
@@ -20983,7 +20983,7 @@ else
 {
 lean_object* x_52; lean_object* x_53; 
 lean_dec(x_46);
-x_52 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_52 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_52, x_42);
 x_16 = x_53;
 goto block_36;
@@ -20993,7 +20993,7 @@ else
 {
 lean_object* x_54; lean_object* x_55; 
 lean_dec(x_44);
-x_54 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_54 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_55 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_54, x_42);
 x_16 = x_55;
 goto block_36;
@@ -21050,13 +21050,13 @@ lean_object* x_70; lean_object* x_71; uint8_t x_72;
 x_70 = lean_ctor_get(x_69, 1);
 lean_inc(x_70);
 lean_dec(x_69);
-x_71 = l_Lean_Parser_Term_listLit___elambda__1___closed__5;
+x_71 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5;
 x_72 = lean_string_dec_eq(x_70, x_71);
 lean_dec(x_70);
 if (x_72 == 0)
 {
 lean_object* x_73; lean_object* x_74; 
-x_73 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_73 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 x_74 = l_Lean_Parser_ParserState_mkErrorsAt(x_66, x_73, x_65);
 x_37 = x_74;
 goto block_62;
@@ -21072,7 +21072,7 @@ else
 {
 lean_object* x_75; lean_object* x_76; 
 lean_dec(x_69);
-x_75 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_75 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 x_76 = l_Lean_Parser_ParserState_mkErrorsAt(x_66, x_75, x_65);
 x_37 = x_76;
 goto block_62;
@@ -21082,7 +21082,7 @@ else
 {
 lean_object* x_77; lean_object* x_78; 
 lean_dec(x_67);
-x_77 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_77 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 x_78 = l_Lean_Parser_ParserState_mkErrorsAt(x_66, x_77, x_65);
 x_37 = x_78;
 goto block_62;
@@ -21261,7 +21261,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_ident;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_listLit___closed__4;
+x_3 = l_Lean_Parser_Term_structInstArrayRef___closed__2;
 x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
 return x_4;
 }
@@ -21280,7 +21280,7 @@ lean_object* _init_l_Lean_Parser_Command_attribute___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_instBinder___closed__1;
+x_1 = l_Lean_Parser_Term_structInstArrayRef___closed__1;
 x_2 = l_Lean_Parser_Command_attribute___closed__5;
 x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;

stage0/stdlib/Init/Lean/Parser/Syntax.c

@@ -142,12 +142,10 @@ lean_object* l_Lean_Parser_Command_infixr;
 lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__6;
-extern lean_object* l_Lean_Parser_Term_listLit___closed__4;
 lean_object* l_Lean_Parser_Command_macroTailDefault___elambda__1(lean_object*, lean_object*);
 lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*);
 lean_object* l_Lean_Parser_maxPrec___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__3;
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_macroHead___closed__1;
@@ -300,6 +298,7 @@ lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1(lean_object*, lean_obj
 extern lean_object* l_Lean_Parser_Term_tacticStxQuot___closed__2;
 extern lean_object* l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Syntax_paren___closed__5;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__1;
 lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__4;
@@ -404,7 +403,6 @@ extern lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__1;
 lean_object* l_Lean_Parser_Command_reserve___closed__4;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_paren(lean_object*);
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__4;
 extern lean_object* l_Lean_Parser_Term_str___elambda__1___closed__1;
@@ -433,6 +431,7 @@ lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
 extern lean_object* l_Lean_Parser_numLit;
 lean_object* l_Lean_Parser_Syntax_num___elambda__1___closed__2;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__2;
 lean_object* l_Lean_Parser_Syntax_paren___closed__2;
 lean_object* l_Lean_Parser_Command_mixfixKind___elambda__1(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_haveAssign___closed__1;
@@ -446,7 +445,6 @@ lean_object* l_Lean_Parser_Command_macro;
 lean_object* l_Lean_Parser_Command_syntax___closed__6;
 lean_object* l_Lean_Parser_Syntax_str___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1___closed__2;
-extern lean_object* l_Lean_Parser_Term_instBinder___closed__1;
 lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__1;
 lean_object* l_Lean_Parser_precedence___closed__5;
 lean_object* l_Lean_Parser_Syntax_optional___closed__3;
@@ -463,7 +461,7 @@ lean_object* l_Lean_Parser_Syntax_cat___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_reserve___closed__6;
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__1;
 extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__2;
 lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__3;
@@ -524,6 +522,7 @@ lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__3;
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__5;
 lean_object* l_Lean_Parser_Command_notation___closed__9;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Syntax_atom___elambda__1___closed__3;
@@ -598,6 +597,7 @@ lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_macro__rules___closed__2;
 lean_object* l_Lean_Parser_Command_syntax___closed__9;
 lean_object* l_Lean_Parser_Command_macroTailDefault___closed__2;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Syntax_atom___closed__2;
 lean_object* l_Lean_Parser_precedence___closed__2;
 lean_object* l_Lean_Parser_Syntax_char___elambda__1(lean_object*, lean_object*);
@@ -644,6 +644,7 @@ lean_object* l_Lean_Parser_Syntax_atom___closed__3;
 lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__5;
 extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Syntax_orelse___closed__4;
+extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Command_syntax___closed__8;
 lean_object* l_Lean_Parser_precedence___closed__4;
 lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__4;
@@ -673,7 +674,6 @@ lean_object* l_Lean_Parser_Command_mixfix___closed__7;
 lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_syntaxCat___closed__2;
 lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__6;
-extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_macroTailCommand___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_maxPrec___closed__2;
 lean_object* l_Lean_Parser_optPrecedence___closed__1;
@@ -7721,13 +7721,13 @@ lean_object* x_41; lean_object* x_42; uint8_t x_43;
 x_41 = lean_ctor_get(x_40, 1);
 lean_inc(x_41);
 lean_dec(x_40);
-x_42 = l_Lean_Parser_Term_listLit___elambda__1___closed__5;
+x_42 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5;
 x_43 = lean_string_dec_eq(x_41, x_42);
 lean_dec(x_41);
 if (x_43 == 0)
 {
 lean_object* x_44; lean_object* x_45; 
-x_44 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_44 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_inc(x_5);
 x_45 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_44, x_5);
 x_18 = x_45;
@@ -7743,7 +7743,7 @@ else
 {
 lean_object* x_46; lean_object* x_47; 
 lean_dec(x_40);
-x_46 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_46 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_inc(x_5);
 x_47 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_46, x_5);
 x_18 = x_47;
@@ -7754,7 +7754,7 @@ else
 {
 lean_object* x_48; lean_object* x_49; 
 lean_dec(x_38);
-x_48 = l_Lean_Parser_Term_listLit___elambda__1___closed__12;
+x_48 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__12;
 lean_inc(x_5);
 x_49 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_48, x_5);
 x_18 = x_49;
@@ -7832,13 +7832,13 @@ lean_object* x_27; lean_object* x_28; uint8_t x_29;
 x_27 = lean_ctor_get(x_26, 1);
 lean_inc(x_27);
 lean_dec(x_26);
-x_28 = l_Lean_Parser_Term_listLit___elambda__1___closed__6;
+x_28 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6;
 x_29 = lean_string_dec_eq(x_27, x_28);
 lean_dec(x_27);
 if (x_29 == 0)
 {
 lean_object* x_30; lean_object* x_31; 
-x_30 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_30 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_30, x_22);
 x_6 = x_31;
 goto block_17;
@@ -7854,7 +7854,7 @@ else
 {
 lean_object* x_32; lean_object* x_33; 
 lean_dec(x_26);
-x_32 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_32 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_33 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_32, x_22);
 x_6 = x_33;
 goto block_17;
@@ -7864,7 +7864,7 @@ else
 {
 lean_object* x_34; lean_object* x_35; 
 lean_dec(x_24);
-x_34 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_34 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
 x_35 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_34, x_22);
 x_6 = x_35;
 goto block_17;
@@ -7895,7 +7895,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_ident;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_listLit___closed__4;
+x_3 = l_Lean_Parser_Term_structInstArrayRef___closed__2;
 x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
 return x_4;
 }
@@ -7904,7 +7904,7 @@ lean_object* _init_l_Lean_Parser_Command_optKind___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_instBinder___closed__1;
+x_1 = l_Lean_Parser_Term_structInstArrayRef___closed__1;
 x_2 = l_Lean_Parser_Command_optKind___closed__1;
 x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;