chore: update stage0

stage0/src/Init/System/IO.lean

@@ -165,6 +165,9 @@ def lazyPure (fn : Unit → α) : IO α :=
 /-- Monotonically increasing time since an unspecified past point in milliseconds. No relation to wall clock time. -/
 @[extern "lean_io_mono_ms_now"] constant monoMsNow : BaseIO Nat
 
+/-- Monotonically increasing time since an unspecified past point in nanoseconds. No relation to wall clock time. -/
+@[extern "lean_io_mono_nanos_now"] constant monoNanosNow : BaseIO Nat
+
 /-- Read bytes from a system entropy source. Not guaranteed to be cryptographically secure.
 If `nBytes = 0`, return immediately with an empty buffer. -/
 @[extern "lean_io_get_random_bytes"] constant getRandomBytes (nBytes : USize) : IO ByteArray

stage0/src/Lean/Data/FuzzyMatching.lean

@@ -182,10 +182,6 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
       /- Match starts in the middle of a segment. -/
       if wordRole matches CharRole.tail && !consecutive then
         score := score - 3
-      /- Beginning of a segment in the pattern is not aligned with the
-      beginning of a segment in the word. -/
-      if patternRole matches CharRole.head && wordRole matches CharRole.tail then
-        score := score - 1
 
       return score
 

stage0/src/Lean/Elab/App.lean

@@ -827,6 +827,33 @@ where
     | field::fields, true  => LVal.fieldName field field.getId.toString (toName (field::fields)) fIdent :: toLVals fields false
     | field::fields, false => LVal.fieldName field field.getId.toString none fIdent :: toLVals fields false
 
+/-- Resolve `(.$id:ident)` using the expected type to infer namespace. -/
+private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Name := do
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType := expectedType?
+    | throwError "invalid dotted identifier notation, expected type must be known"
+  forallTelescopeReducing expectedType fun _ resultType => do
+    go resultType expectedType #[]
+where
+  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Name := do
+    let resultTypeFn := (← instantiateMVars resultType).consumeMData.getAppFn
+    try
+      tryPostponeIfMVar resultTypeFn
+      let .const declName .. := resultTypeFn.consumeMData
+        | throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
+      let idNew := declName ++ id.getId.eraseMacroScopes
+      unless (← getEnv).contains idNew do
+        throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+      return idNew
+    catch
+      | ex@(.error _ _) =>
+        match (← unfoldDefinition? resultType) with
+        | some resultType => go (← whnfCore resultType) expectedType (previousExceptions.push ex)
+        | none       =>
+          previousExceptions.forM fun ex => logException ex
+          throw ex
+      | ex@(.internal _ _) => throw ex
+
 private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg)
     (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) : TermElabM (Array (TermElabResult Expr)) := do
   if f.getKind == choiceKind then
@@ -862,18 +889,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `(@$t)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
     | `(.$id:ident) =>
-      tryPostponeIfNoneOrMVar expectedType?
-      let some expectedType := expectedType?
-        | throwError "invalid dotted identifier notation, expected type must be known"
-      forallTelescopeReducing expectedType fun _ resultType => do
-        let resultTypeFn := (← instantiateMVars resultType).consumeMData.getAppFn
-        tryPostponeIfMVar resultTypeFn
-        let .const declName .. := resultTypeFn.consumeMData
-          | throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
-        let idNew := declName ++ id.getId.eraseMacroScopes
-        unless (← getEnv).contains idNew do
-          throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
-        let fConst ← mkConst idNew
+        let fConst ← mkConst (← resolveDotName id expectedType?)
         let fConst ← addTermInfo f fConst
         let s ← observing do
           let e ← elabAppLVals fConst lvals namedArgs args expectedType? explicit ellipsis

stage0/src/Lean/Elab/Inductive.lean

@@ -269,6 +269,16 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
       let binderNames := getArrowBinderNames (← instantiateMVars (← inferType C))
       return replaceArrowBinderNames r binderNames[:bsPrefix.size]
 
+/--
+  Execute `k` with updated binder information for `xs`. Any `x` that is explicit becomes implicit.
+-/
+private def withExplicitToImplicit (xs : Array Expr) (k : TermElabM α) : TermElabM α := do
+  let mut toImplicit := #[]
+  for x in xs do
+    if (← getFVarLocalDecl x).binderInfo.isExplicit then
+      toImplicit := toImplicit.push (x.fvarId!, BinderInfo.implicit)
+  withNewBinderInfos toImplicit k
+
 /-
   Elaborate constructor types.
 
@@ -314,7 +324,7 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
           let type  ← mkForallFVars (extraCtorParams ++ ctorParams) type
           let type ← reorderCtorArgs type
           let type ← mkForallFVars params type
-          trace[Elab.inductive] "{ctorView.declName} : {type} "
+          trace[Elab.inductive] "{ctorView.declName} : {type}"
           return { name := ctorView.declName, type }
 where
   checkParamOccs (ctorType : Expr) : MetaM Expr :=
@@ -522,7 +532,7 @@ private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : T
   indTypes.mapM fun indType => do
     let type ← mkForallFVars vars indType.type
     let ctors ← indType.ctors.mapM fun ctor => do
-      let ctorType ← mkForallFVars vars ctor.type
+      let ctorType ← withExplicitToImplicit vars (mkForallFVars vars ctor.type)
       return { ctor with type := ctorType }
     return { indType with type := type, ctors := ctors }
 
@@ -561,24 +571,6 @@ private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars :
       return { ctor with type := type }
     return { indType with ctors := ctors }
 
-abbrev Ctor2InferMod := Std.HashMap Name Bool
-
-private def mkCtor2InferMod (views : Array InductiveView) : Ctor2InferMod := Id.run do
-  let mut m := {}
-  for view in views do
-    for ctorView in view.ctors do
-      m := m.insert ctorView.declName ctorView.inferMod
-  return m
-
-private def applyInferMod (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : List InductiveType :=
-  let ctor2InferMod := mkCtor2InferMod views
-  indTypes.map fun indType =>
-    let ctors := indType.ctors.map fun ctor =>
-      let inferMod := ctor2InferMod.find! ctor.name -- true if `{}` was used
-      let ctorType := ctor.type.inferImplicit numParams !inferMod
-      { ctor with type := ctorType }
-    { indType with ctors := ctors }
-
 private def mkAuxConstructions (views : Array InductiveView) : TermElabM Unit := do
   let env ← getEnv
   let hasEq   := env.contains ``Eq
@@ -640,16 +632,26 @@ private def isDomainDefEq (arrowType : Expr) (type : Expr) : MetaM Bool := do
   if !arrowType.isForall then
     return false
   else
-    withNewMCtxDepth do -- Make sure we do not assign univers metavariables
-      isDefEq arrowType.bindingDomain! type
+    /-
+      We used to use `withNewMCtxDepth` to make sure we do not assign universe metavariables,
+      but it was not satisfactory. For example, in declarations such as
+      ```
+      inductive Eq : α → α → Prop where
+      | refl (a : α) : Eq a a
+      ```
+      We want the first two indices to be promoted to parameters, and this will only
+      happen if we can assign universe metavariables.
+    -/
+    isDefEq arrowType.bindingDomain! type
 
 /--
   Convert fixed indices to parameters.
 -/
-private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveType) (indFVars : Array Expr) : MetaM (Nat × List InductiveType) := do
+private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveType) (indFVars : Array Expr) : MetaM Nat := do
   let masks ← indTypes.mapM (computeFixedIndexBitMask numParams · indFVars)
   if masks.all fun mask => !mask.contains true then
-    return (numParams, indTypes.toList)
+    return numParams
+  trace[Elab.inductive] "masks: {masks}"
   -- We process just a non-fixed prefix of the indices for now. Reason: we don't want to change the order.
   -- TODO: extend it in the future. For example, it should be reasonable to change
   -- the order of indices generated by the auto implicit feature.
@@ -658,7 +660,7 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind
     let otherTypes ← indTypes[1:].toArray.mapM fun indType => do whnfD (← instantiateForall indType.type params)
     let ctorTypes ← indTypes.toList.mapM fun indType => indType.ctors.mapM fun ctor => do whnfD (← instantiateForall ctor.type params)
     let typesToCheck := otherTypes.toList ++ ctorTypes.join
-    let rec go (i : Nat) (typesToCheck : List Expr) : MetaM Nat := do
+    let rec go (i : Nat) (type : Expr) (typesToCheck : List Expr) : MetaM Nat := do
       if i < mask.size then
         if !masks.all fun mask => i < mask.size && mask[i] then
            return i
@@ -666,13 +668,14 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind
           return i
         let paramType := type.bindingDomain!
         if !(← typesToCheck.allM fun type => isDomainDefEq type paramType) then
+          trace[Elab.inductive] "domain not def eq: {i}, {type} =?= {paramType}"
           return i
         withLocalDeclD `a paramType fun paramNew => do
           let typesToCheck ← typesToCheck.mapM fun type => whnfD (type.bindingBody!.instantiate1 paramNew)
-          go (i+1) typesToCheck
+          go (i+1) (type.bindingBody!.instantiate1 paramNew) typesToCheck
       else
         return i
-    return (← go numParams typesToCheck, indTypes.toList)
+    go numParams type typesToCheck
 
 private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do
   let view0 := views[0]
@@ -689,10 +692,12 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
         Term.addLocalVarInfo views[i].declId indFVar
         let r       := rs[i]
         let type  ← mkForallFVars params r.type
-        let ctors ← elabCtors indFVars indFVar params r
+        let ctors ← withExplicitToImplicit params (elabCtors indFVars indFVar params r)
         indTypesArray := indTypesArray.push { name := r.view.declName, type := type, ctors := ctors : InductiveType }
       Term.synthesizeSyntheticMVarsNoPostponing
-      let (numExplicitParams, indTypes) ← fixedIndicesToParams params.size indTypesArray indFVars
+      let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars
+      trace[Elab.inductive] "numExplicitParams: {numExplicitParams}"
+      let indTypes := indTypesArray.toList
       let u ← getResultingUniverse indTypes
       let univToInfer? ← shouldInferResultUniverse u
       withUsed vars indTypes fun vars => do
@@ -710,7 +715,6 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
         | Except.error msg      => throwError msg
         | Except.ok levelParams => do
           let indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes
-          let indTypes := applyInferMod views numParams indTypes
           let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe
           Term.ensureNoUnassignedMVars decl
           addDecl decl

stage0/src/Lean/Elab/Match.lean

@@ -605,16 +605,30 @@ where
 /--
   Save pattern information in the info tree, and remove `patternWithRef?` annotations.
 -/
-def savePatternInfo (p : Expr) : TermElabM Expr :=
-  withReader (fun ctx => { ctx with inPattern := false }) do
-    let post (e : Expr) : TermElabM TransformStep := do
-      if let some (stx, e) := patternWithRef? e then
-        -- TODO: track whether we are inside of an inaccessible, and set `isBinder`
-        addTermInfo' stx e
-        return .done e
+partial def savePatternInfo (p : Expr) : TermElabM Expr :=
+  go p |>.run false
+where
+  /- The `Bool` context is true iff we are inside of an "inaccessible" pattern. -/
+  go (p : Expr) : ReaderT Bool TermElabM Expr := do
+    match p with
+    | .forallE n d b bi => withLocalDecl n b.binderInfo (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x))
+    | .lam n d b bi     => withLocalDecl n b.binderInfo (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x))
+    | .letE n t v b ..  => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
+    | .app f a _        => return mkApp (← go f) (← go a)
+    | .proj _ _ b _     => return p.updateProj! (← go b)
+    | .mdata k b _      =>
+      if inaccessible? p |>.isSome then
+        return mkMData k (← withReader (fun _ => false) (go b))
+      else if let some (stx, p) := patternWithRef? p then
+        let p ← go p
+        if p.isFVar && !(← read) then
+          /- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/
+          addTermInfo stx p (isBinder := true)
+        else
+          addTermInfo stx p
       else
-        return .done e
-    transform p (post := post)
+        return mkMData k (← go b)
+    | _ => return p
 
 /--
   Main method for `withDepElimPatterns`.

stage0/src/Lean/Elab/Tactic/Config.lean

@@ -16,7 +16,7 @@ macro "declare_config_elab" elabName:ident type:ident : command =>
      if optConfig.isNone then
        return { : $type }
      else
-       withoutModifyingState <| withLCtx {} {} <| Term.withSynthesize do
+       withoutModifyingState <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do
          let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type)
          eval (← instantiateMVars c)
   )

stage0/src/Lean/Elab/Term.lean

@@ -305,7 +305,7 @@ def withoutModifyingElabMetaStateWithInfo (x : TermElabM α) : TermElabM α := d
 private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : TermElabM α := do
   let saved ← saveState
   try
-    x
+    withSaveInfoContext x
   finally
     let s ← get
     let saved := { saved with elab.infoState := s.infoState, elab.messages := s.messages }
@@ -1492,40 +1492,25 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
    return (const, projs) :: result
 
 def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
-  try
-    if let some (e, projs) ← resolveLocalName n then
-      if (← read).autoBoundImplicit then
-        /- We used to generate completion info nodes only for names that could not be resolved.
-           However, this is very unsatisfactory for when elaborating headers when `autoBoundImplicit` is turned on.
-           The problem is that new local declarations are introduced by `autoBoundImplicit` and we eventually can always resolve the name.
-           Thus, we add the completion info in this case.
-           TODO: revisit this design decision. Alternative design: always create a completion info node.
-           Note that in the current design if a constant name is a prefix of another one, we will not have a completion info node.
-        -/
-        addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
-      unless explicitLevels.isEmpty do
-        throwError "invalid use of explicit universe parameters, '{e}' is a local"
-      return [(e, projs)]
-    -- check for section variable capture by a quotation
-    let ctx ← read
-    if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
-      return [(e, projs)]  -- section variables should shadow global decls
-    if preresolved.isEmpty then
-      process (← resolveGlobalName n)
-    else
-      process preresolved
-  catch ex =>
-    if preresolved.isEmpty && explicitLevels.isEmpty then
-      addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
-    throw ex
+  addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
+  if let some (e, projs) ← resolveLocalName n then
+    unless explicitLevels.isEmpty do
+      throwError "invalid use of explicit universe parameters, '{e}' is a local"
+    return [(e, projs)]
+  -- check for section variable capture by a quotation
+  let ctx ← read
+  if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
+    return [(e, projs)]  -- section variables should shadow global decls
+  if preresolved.isEmpty then
+    process (← resolveGlobalName n)
+  else
+    process preresolved
 where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
   if candidates.isEmpty then
     if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
       throwAutoBoundImplicitLocal n
     else
       throwError "unknown identifier '{Lean.mkConst n}'"
-  if preresolved.isEmpty && explicitLevels.isEmpty then
-    addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
   mkConsts candidates explicitLevels
 
 /--

stage0/src/Lean/Meta/AppBuilder.lean

@@ -363,33 +363,32 @@ def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=
 /--
   `mkProjection s fieldName` return an expression for accessing field `fieldName` of the structure `s`.
   Remark: `fieldName` may be a subfield of `s`. -/
-partial def mkProjection : Expr → Name → MetaM Expr
-  | s, fieldName => do
-    let type ← inferType s
-    let type ← whnf type
-    match type.getAppFn with
-    | Expr.const structName us _ =>
-      let env ← getEnv
-      unless isStructure env structName do
-        throwAppBuilderException `mkProjection ("structure expected" ++ hasTypeMsg s type)
-      match getProjFnForField? env structName fieldName with
-      | some projFn =>
-        let params := type.getAppArgs
-        return mkApp (mkAppN (mkConst projFn us) params) s
-      | none =>
-        let fields := getStructureFields env structName
-        let r? ← fields.findSomeM? fun fieldName' => do
-          match isSubobjectField? env structName fieldName' with
-          | none   => pure none
-          | some _ =>
-            let parent ← mkProjection s fieldName'
-            (do let r ← mkProjection parent fieldName; return some r)
-            <|>
-            pure none
-        match r? with
-        | some r => pure r
-        | none   => throwAppBuilderException `mkProjectionn ("invalid field name '" ++ toString fieldName ++ "' for" ++ hasTypeMsg s type)
-    | _ => throwAppBuilderException `mkProjectionn ("structure expected" ++ hasTypeMsg s type)
+partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
+  let type ← inferType s
+  let type ← whnf type
+  match type.getAppFn with
+  | Expr.const structName us _ =>
+    let env ← getEnv
+    unless isStructure env structName do
+      throwAppBuilderException `mkProjection ("structure expected" ++ hasTypeMsg s type)
+    match getProjFnForField? env structName fieldName with
+    | some projFn =>
+      let params := type.getAppArgs
+      return mkApp (mkAppN (mkConst projFn us) params) s
+    | none =>
+      let fields := getStructureFields env structName
+      let r? ← fields.findSomeM? fun fieldName' => do
+        match isSubobjectField? env structName fieldName' with
+        | none   => pure none
+        | some _ =>
+          let parent ← mkProjection s fieldName'
+          (do let r ← mkProjection parent fieldName; return some r)
+          <|>
+          pure none
+      match r? with
+      | some r => pure r
+      | none   => throwAppBuilderException `mkProjectionn ("invalid field name '" ++ toString fieldName ++ "' for" ++ hasTypeMsg s type)
+  | _ => throwAppBuilderException `mkProjectionn ("structure expected" ++ hasTypeMsg s type)
 
 private def mkListLitAux (nil : Expr) (cons : Expr) : List Expr → Expr
   | []    => nil

stage0/src/Lean/Meta/ExprDefEq.lean

@@ -36,10 +36,10 @@ namespace Lean.Meta
 private def isDefEqEtaStruct (a b : Expr) : MetaM Bool := do
   if !(← getConfig).etaStruct then return false
   else
-    matchConstCtor b.getAppFn (fun _ => return false) fun ctorVal _ =>
-    matchConstCtor a.getAppFn (fun _ => go ctorVal) fun _ _ => return false
+    matchConstCtor b.getAppFn (fun _ => return false) fun ctorVal us =>
+    matchConstCtor a.getAppFn (fun _ => go ctorVal us) fun _ _ => return false
 where
-  go ctorVal := do
+  go ctorVal us := do
     if ctorVal.numParams + ctorVal.numFields != b.getAppNumArgs then
       trace[Meta.isDefEq.eta.struct] "failed, insufficient number of arguments at{indentExpr b}"
       return false
@@ -50,9 +50,12 @@ where
       else if (← isDefEq (← inferType a) (← inferType b)) then
         checkpointDefEq do
           let args := b.getAppArgs
+          let params := args[:ctorVal.numParams].toArray
+          let info? := getStructureInfo? (← getEnv) ctorVal.induct
           for i in [ctorVal.numParams : args.size] do
-            let proj := mkProj ctorVal.induct (i - ctorVal.numParams) a
-            trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{i - ctorVal.numParams}], {proj} =?= {args[i]}"
+            let j := i - ctorVal.numParams
+            let proj ← mkProjFn ctorVal us params j a
+            trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]}"
             unless (← isDefEq proj args[i]) do
               trace[Meta.isDefEq.eta.struct] "failed, unexpect arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]}"
               return false

stage0/src/Lean/Meta/Tactic/Simp/Main.lean

@@ -680,9 +680,9 @@ def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Si
       else
         return some (proof, r.expr)
 
-def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) : MetaM (Option (Expr × Expr)) := do
+def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (Expr × Expr)) := do
   let localDecl ← getLocalDecl fvarId
-  applySimpResultToProp mvarId (mkFVar fvarId) localDecl.type r
+  applySimpResultToProp mvarId (mkFVar fvarId) localDecl.type r mayCloseGoal
 
 /--
   Simplify `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@@ -709,8 +709,17 @@ def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Opti
 /--
   Simplify `simp` result to the given local declaration. Return `none` if the goal was closed.
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) : MetaM (Option (FVarId × MVarId)) := do
-  applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r)
+def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (FVarId × MVarId)) := do
+  if r.proof?.isNone then
+    -- New result is definitionally equal to input. Thus, we can avoid creating a new variable if there are dependencies
+    let mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr
+    if mayCloseGoal && r.expr.isConstOf ``False then
+      assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId))
+      return none
+    else
+      return some (fvarId, mvarId)
+  else
+    applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
 def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option (FVarId × MVarId)) := do
   withMVarContext mvarId do
@@ -725,22 +734,34 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
   withMVarContext mvarId do
     checkNotAssigned mvarId `simp
     let mut mvarId := mvarId
-    let mut toAssert : Array Hypothesis := #[]
+    let mut toAssert := #[]
+    let mut replaced := #[]
     for fvarId in fvarIdsToSimp do
       let localDecl ← getLocalDecl fvarId
       let type ← instantiateMVars localDecl.type
       let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
         | none => pure ctx
         | some thmId => pure { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem thmId }
-      match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
-      | none => return none
-      | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
-    if simplifyTarget then
+      let r ← simp type ctx discharge?
+      match r.proof? with
+      | some proof => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
+        | none => return none
+        | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
+      | none =>
+        if r.expr.isConstOf ``False then
+          assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId))
+          return none
+        -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
+        -- Reason: it introduces a `mkExpectedTypeHint`
+        mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr
+        replaced := replaced.push fvarId
+     if simplifyTarget then
       match (← simpTarget mvarId ctx discharge?) with
       | none => return none
       | some mvarIdNew => mvarId := mvarIdNew
     let (fvarIdsNew, mvarIdNew) ← assertHypotheses mvarId toAssert
-    let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
+    let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
+    let mvarIdNew ← tryClearMany mvarIdNew toClear
     return (fvarIdsNew, mvarIdNew)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM TacticResultCNM := withMVarContext mvarId do

stage0/src/Lean/Meta/Tactic/Unfold.lean

@@ -36,7 +36,7 @@ def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := withMVarC
 def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do
   let localDecl ← getLocalDecl fvarId
   let r ← unfold (← instantiateMVars localDecl.type) declName
-  let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r | unreachable!
+  let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable!
   return mvarId
 
 end Lean.Meta

stage0/src/Lean/Meta/WHNF.lean

@@ -115,6 +115,17 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
     else
       return major
 
+/--
+  Create the `i`th projection `major`. It tries to use the auto-generated projection functions if available. Otherwise falls back
+  to `Expr.proj`.
+-/
+def mkProjFn (ctorVal : ConstructorVal) (us : List Level) (params : Array Expr) (i : Nat) (major : Expr) : CoreM Expr := do
+  match getStructureInfo? (← getEnv) ctorVal.induct with
+  | none => return mkProj ctorVal.induct i major
+  | some info => match info.getProjFn? i with
+    | none => return mkProj ctorVal.induct i major
+    | some projFn => return mkApp (mkAppN (mkConst projFn us) params) major
+
 /--
   If `major` is not a constructor application, and its type is a structure `C ...`, then return `C.mk major.1 ... major.n`
 
@@ -142,9 +153,10 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr
       else
         let some ctorName ← getFirstCtor d | pure major
         let ctorInfo ← getConstInfoCtor ctorName
-        let mut result := mkAppN (mkConst ctorName us) (majorType.getAppArgs.shrink ctorInfo.numParams)
+        let params := majorType.getAppArgs.shrink ctorInfo.numParams
+        let mut result := mkAppN (mkConst ctorName us) params
         for i in [:ctorInfo.numFields] do
-          result := mkApp result (mkProj inductName i major)
+          result := mkApp result (← mkProjFn ctorInfo us params i major)
         return result
     | _ => return major
 

stage0/src/Lean/Server/Watchdog.lean

@@ -394,9 +394,11 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
   return result
 
 def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInformation) := do
+  if p.query.isEmpty then
+    return #[]
   let references ← (← read).references.get
   let srcSearchPath := (← read).srcSearchPath
-  let symbols ← references.definitionsMatching srcSearchPath (maxAmount? := some 100)
+  let symbols ← references.definitionsMatching srcSearchPath (maxAmount? := none)
     fun name =>
       let name := privateToUserName? name |>.getD name
       if let some score := fuzzyMatchScoreWithThreshold? p.query name.toString then
@@ -405,6 +407,7 @@ def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInf
         none
   return symbols
     |>.qsort (fun ((_, s1), _) ((_, s2), _) => s1 > s2)
+    |>.extract 0 100 -- max amount
     |>.map fun ((name, score), location) =>
       { name, kind := SymbolKind.constant, location }
 

stage0/src/Lean/Structure.lean

@@ -30,6 +30,13 @@ structure StructureInfo where
 def StructureInfo.lt (i₁ i₂ : StructureInfo) : Bool :=
   Name.quickLt i₁.structName i₂.structName
 
+def StructureInfo.getProjFn? (info : StructureInfo) (i : Nat) : Option Name :=
+  if h : i < info.fieldNames.size then
+    let fieldName := info.fieldNames.get ⟨i, h⟩
+    info.fieldInfo.binSearch { fieldName := fieldName, projFn := default, subobject? := none, binderInfo := default, inferMod := false } StructureFieldInfo.lt |>.map (·.projFn)
+  else
+    none
+
 /-- Auxiliary state for structures defined in the current module. -/
 private structure StructureState where
   map : Std.PersistentHashMap Name StructureInfo := {}

stage0/src/runtime/io.cpp

@@ -360,9 +360,18 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_ar
 
 /* monoMsNow : BaseIO Nat */
 extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now(obj_arg /* w */) {
+    static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64));
     auto now = std::chrono::steady_clock::now();
     auto tm = std::chrono::duration_cast<std::chrono::milliseconds>(now.time_since_epoch());
-    return io_result_mk_ok(usize_to_nat(tm.count()));
+    return io_result_mk_ok(uint64_to_nat(tm.count()));
+}
+
+/* monoNanosNow : BaseIO Nat */
+extern "C" LEAN_EXPORT obj_res lean_io_mono_nanos_now(obj_arg /* w */) {
+    static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64));
+    auto now = std::chrono::steady_clock::now();
+    auto tm = std::chrono::duration_cast<std::chrono::nanoseconds>(now.time_since_epoch());
+    return io_result_mk_ok(uint64_to_nat(tm.count()));
 }
 
 /* getRandomBytes (nBytes : USize) : IO ByteArray */

stage0/stdlib/Lean/Data/FuzzyMatching.c

@@ -14,7 +14,6 @@
 extern "C" {
 #endif
 LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_containsInOrderLower___lambda__2(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_skipPenalty___lambda__1___boxed(lean_object*);
 lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_getMiss(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -29,7 +28,6 @@ static lean_object* l_Lean_FuzzyMatching_fuzzyMatchScore_x3f___lambda__1___close
 LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static uint8_t l_Lean_FuzzyMatching_fuzzyMatchScore_x3f___lambda__1___closed__5;
 LEAN_EXPORT lean_object* l_Lean_FuzzyMatching_CharType_toCtorIdx(uint8_t);
-LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4(uint8_t, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_FuzzyMatching_charRole(lean_object*, uint8_t, lean_object*);
 static lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_iterateLookaround___rarg___closed__2;
 LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_iterateLookaround___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1799,61 +1797,23 @@ _start:
 lean_object* x_5; lean_object* x_6; 
 x_5 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__2___closed__1;
 x_6 = lean_box(x_1);
-if (lean_obj_tag(x_6) == 0)
-{
-lean_object* x_7; 
-x_7 = lean_box(x_2);
-if (lean_obj_tag(x_7) == 1)
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_8 = lean_unsigned_to_nat(1u);
-x_9 = lean_nat_sub(x_3, x_8);
-lean_dec(x_3);
-x_10 = lean_box(0);
-x_11 = lean_apply_2(x_5, x_9, x_10);
-return x_11;
-}
-else
-{
-lean_object* x_12; lean_object* x_13; 
-lean_dec(x_7);
-x_12 = lean_box(0);
-x_13 = lean_apply_2(x_5, x_3, x_12);
-return x_13;
-}
-}
-else
-{
-lean_object* x_14; lean_object* x_15; 
-lean_dec(x_6);
-x_14 = lean_box(0);
-x_15 = lean_apply_2(x_5, x_3, x_14);
-return x_15;
-}
-}
-}
-LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(uint8_t x_1, uint8_t x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5) {
-_start:
-{
-lean_object* x_6; 
-x_6 = lean_box(x_2);
 if (lean_obj_tag(x_6) == 1)
 {
-if (x_3 == 0)
+if (x_2 == 0)
 {
 lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
 x_7 = lean_unsigned_to_nat(3u);
-x_8 = lean_nat_sub(x_4, x_7);
-lean_dec(x_4);
+x_8 = lean_nat_sub(x_3, x_7);
+lean_dec(x_3);
 x_9 = lean_box(0);
-x_10 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__2(x_1, x_2, x_8, x_9);
+x_10 = lean_apply_2(x_5, x_8, x_9);
 return x_10;
 }
 else
 {
 lean_object* x_11; lean_object* x_12; 
 x_11 = lean_box(0);
-x_12 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__2(x_1, x_2, x_4, x_11);
+x_12 = lean_apply_2(x_5, x_3, x_11);
 return x_12;
 }
 }
@@ -1862,43 +1822,43 @@ else
 lean_object* x_13; lean_object* x_14; 
 lean_dec(x_6);
 x_13 = lean_box(0);
-x_14 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__2(x_1, x_2, x_4, x_13);
+x_14 = lean_apply_2(x_5, x_3, x_13);
 return x_14;
 }
 }
 }
-LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4(uint8_t x_1, uint8_t x_2, uint8_t x_3, uint8_t x_4, lean_object* x_5, lean_object* x_6) {
+LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(uint8_t x_1, uint8_t x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-if (x_4 == 0)
-{
 if (x_3 == 0)
 {
-lean_object* x_7; lean_object* x_8; 
-x_7 = lean_box(0);
-x_8 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(x_1, x_2, x_3, x_5, x_7);
-return x_8;
+if (x_2 == 0)
+{
+lean_object* x_6; lean_object* x_7; 
+x_6 = lean_box(0);
+x_7 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__2(x_1, x_2, x_4, x_6);
+return x_7;
 }
 else
 {
-lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_9 = lean_unsigned_to_nat(2u);
-x_10 = lean_nat_add(x_5, x_9);
-lean_dec(x_5);
-x_11 = lean_box(0);
-x_12 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(x_1, x_2, x_3, x_10, x_11);
-return x_12;
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = lean_unsigned_to_nat(2u);
+x_9 = lean_nat_add(x_4, x_8);
+lean_dec(x_4);
+x_10 = lean_box(0);
+x_11 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__2(x_1, x_2, x_9, x_10);
+return x_11;
 }
 }
 else
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_13 = lean_unsigned_to_nat(2u);
-x_14 = lean_nat_add(x_5, x_13);
-lean_dec(x_5);
-x_15 = lean_box(0);
-x_16 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(x_1, x_2, x_3, x_14, x_15);
-return x_16;
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_12 = lean_unsigned_to_nat(2u);
+x_13 = lean_nat_add(x_4, x_12);
+lean_dec(x_4);
+x_14 = lean_box(0);
+x_15 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__2(x_1, x_2, x_13, x_14);
+return x_15;
 }
 }
 }
@@ -1920,7 +1880,7 @@ if (lean_obj_tag(x_9) == 0)
 lean_object* x_10; lean_object* x_11; lean_object* x_12; 
 x_10 = lean_unsigned_to_nat(2u);
 x_11 = lean_box(0);
-x_12 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4(x_3, x_4, x_5, x_6, x_10, x_11);
+x_12 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(x_4, x_5, x_6, x_10, x_11);
 return x_12;
 }
 else
@@ -1929,7 +1889,7 @@ lean_object* x_13; lean_object* x_14; lean_object* x_15;
 lean_dec(x_9);
 x_13 = lean_unsigned_to_nat(1u);
 x_14 = lean_box(0);
-x_15 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4(x_3, x_4, x_5, x_6, x_13, x_14);
+x_15 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(x_4, x_5, x_6, x_13, x_14);
 return x_15;
 }
 }
@@ -1939,7 +1899,7 @@ lean_object* x_16; lean_object* x_17; lean_object* x_18;
 lean_dec(x_8);
 x_16 = lean_unsigned_to_nat(1u);
 x_17 = lean_box(0);
-x_18 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4(x_3, x_4, x_5, x_6, x_16, x_17);
+x_18 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(x_4, x_5, x_6, x_16, x_17);
 return x_18;
 }
 }
@@ -1948,7 +1908,7 @@ else
 lean_object* x_19; lean_object* x_20; lean_object* x_21; 
 x_19 = lean_unsigned_to_nat(2u);
 x_20 = lean_box(0);
-x_21 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4(x_3, x_4, x_5, x_6, x_19, x_20);
+x_21 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__3(x_4, x_5, x_6, x_19, x_20);
 return x_21;
 }
 }
@@ -1990,23 +1950,6 @@ lean_dec(x_5);
 return x_9;
 }
 }
-LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-uint8_t x_7; uint8_t x_8; uint8_t x_9; uint8_t x_10; lean_object* x_11; 
-x_7 = lean_unbox(x_1);
-lean_dec(x_1);
-x_8 = lean_unbox(x_2);
-lean_dec(x_2);
-x_9 = lean_unbox(x_3);
-lean_dec(x_3);
-x_10 = lean_unbox(x_4);
-lean_dec(x_4);
-x_11 = l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___lambda__4(x_7, x_8, x_9, x_10, x_5, x_6);
-lean_dec(x_6);
-return x_11;
-}
-}
 LEAN_EXPORT lean_object* l___private_Lean_Data_FuzzyMatching_0__Lean_FuzzyMatching_fuzzyMatchCore_matchResult___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {

stage0/stdlib/Lean/Meta/AppBuilder.c

@@ -330,7 +330,7 @@ static lean_object* l_Lean_Meta_mkEqOfHEq___closed__3;
 static lean_object* l_Lean_Meta_mkProjection___lambda__1___closed__9;
 static lean_object* l_Lean_Meta_mkEqMPR___closed__1;
 lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_5672_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_5653_(lean_object*);
 lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewMCtxDepth___at___private_Lean_Meta_Instances_0__Lean_Meta_mkInstanceKey___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -14282,7 +14282,7 @@ x_10 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkBinaryRel(x_8, x_9, x_1,
 return x_10;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_5672_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_5653_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@@ -14754,7 +14754,7 @@ l_Lean_Meta_mkMul___closed__3 = _init_l_Lean_Meta_mkMul___closed__3();
 lean_mark_persistent(l_Lean_Meta_mkMul___closed__3);
 l_Lean_Meta_mkMul___closed__4 = _init_l_Lean_Meta_mkMul___closed__4();
 lean_mark_persistent(l_Lean_Meta_mkMul___closed__4);
-res = l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_5672_(lean_io_mk_world());
+res = l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_5653_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));

stage0/stdlib/Lean/Meta/Tactic/Unfold.c

@@ -13,7 +13,7 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
-lean_object* l_Lean_Meta_applySimpResultToLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_applySimpResultToLocalDecl(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_unfold_pre___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Unfold_0__Lean_Meta_getSimpUnfoldContext___boxed(lean_object*, lean_object*, lean_object*);
@@ -852,7 +852,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
 x_1 = l_Lean_Meta_unfoldLocalDecl___lambda__1___closed__1;
 x_2 = l_Lean_Meta_unfoldLocalDecl___lambda__1___closed__2;
 x_3 = lean_unsigned_to_nat(39u);
-x_4 = lean_unsigned_to_nat(70u);
+x_4 = lean_unsigned_to_nat(94u);
 x_5 = l_Lean_Meta_unfoldLocalDecl___lambda__1___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
 return x_6;
@@ -889,129 +889,130 @@ lean_inc(x_4);
 x_16 = l_Lean_Meta_unfold(x_14, x_2, x_4, x_5, x_6, x_7, x_15);
 if (lean_obj_tag(x_16) == 0)
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20; 
 x_17 = lean_ctor_get(x_16, 0);
 lean_inc(x_17);
 x_18 = lean_ctor_get(x_16, 1);
 lean_inc(x_18);
 lean_dec(x_16);
+x_19 = 0;
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
-x_19 = l_Lean_Meta_applySimpResultToLocalDecl(x_3, x_1, x_17, x_4, x_5, x_6, x_7, x_18);
-if (lean_obj_tag(x_19) == 0)
-{
-lean_object* x_20; 
-x_20 = lean_ctor_get(x_19, 0);
-lean_inc(x_20);
+x_20 = l_Lean_Meta_applySimpResultToLocalDecl(x_3, x_1, x_17, x_19, x_4, x_5, x_6, x_7, x_18);
 if (lean_obj_tag(x_20) == 0)
 {
-lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-x_21 = lean_ctor_get(x_19, 1);
+lean_object* x_21; 
+x_21 = lean_ctor_get(x_20, 0);
 lean_inc(x_21);
-lean_dec(x_19);
-x_22 = l_Lean_Meta_unfoldLocalDecl___lambda__1___closed__4;
-x_23 = l_panic___at_Lean_Meta_unfoldLocalDecl___spec__1(x_22, x_4, x_5, x_6, x_7, x_21);
-return x_23;
-}
-else
+if (lean_obj_tag(x_21) == 0)
 {
-lean_object* x_24; uint8_t x_25; 
-lean_dec(x_7);
-lean_dec(x_6);
-lean_dec(x_5);
-lean_dec(x_4);
-x_24 = lean_ctor_get(x_20, 0);
-lean_inc(x_24);
+lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_22 = lean_ctor_get(x_20, 1);
+lean_inc(x_22);
 lean_dec(x_20);
-x_25 = !lean_is_exclusive(x_19);
-if (x_25 == 0)
-{
-lean_object* x_26; lean_object* x_27; 
-x_26 = lean_ctor_get(x_19, 0);
-lean_dec(x_26);
-x_27 = lean_ctor_get(x_24, 1);
-lean_inc(x_27);
-lean_dec(x_24);
-lean_ctor_set(x_19, 0, x_27);
-return x_19;
+x_23 = l_Lean_Meta_unfoldLocalDecl___lambda__1___closed__4;
+x_24 = l_panic___at_Lean_Meta_unfoldLocalDecl___spec__1(x_23, x_4, x_5, x_6, x_7, x_22);
+return x_24;
 }
 else
 {
-lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-x_28 = lean_ctor_get(x_19, 1);
-lean_inc(x_28);
-lean_dec(x_19);
-x_29 = lean_ctor_get(x_24, 1);
-lean_inc(x_29);
-lean_dec(x_24);
-x_30 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_30, 0, x_29);
-lean_ctor_set(x_30, 1, x_28);
-return x_30;
-}
-}
-}
-else
-{
-uint8_t x_31; 
+lean_object* x_25; uint8_t x_26; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
-x_31 = !lean_is_exclusive(x_19);
-if (x_31 == 0)
+x_25 = lean_ctor_get(x_21, 0);
+lean_inc(x_25);
+lean_dec(x_21);
+x_26 = !lean_is_exclusive(x_20);
+if (x_26 == 0)
 {
-return x_19;
+lean_object* x_27; lean_object* x_28; 
+x_27 = lean_ctor_get(x_20, 0);
+lean_dec(x_27);
+x_28 = lean_ctor_get(x_25, 1);
+lean_inc(x_28);
+lean_dec(x_25);
+lean_ctor_set(x_20, 0, x_28);
+return x_20;
 }
 else
 {
-lean_object* x_32; lean_object* x_33; lean_object* x_34; 
-x_32 = lean_ctor_get(x_19, 0);
-x_33 = lean_ctor_get(x_19, 1);
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_20, 1);
+lean_inc(x_29);
+lean_dec(x_20);
+x_30 = lean_ctor_get(x_25, 1);
+lean_inc(x_30);
+lean_dec(x_25);
+x_31 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_31, 0, x_30);
+lean_ctor_set(x_31, 1, x_29);
+return x_31;
+}
+}
+}
+else
+{
+uint8_t x_32; 
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+x_32 = !lean_is_exclusive(x_20);
+if (x_32 == 0)
+{
+return x_20;
+}
+else
+{
+lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+x_33 = lean_ctor_get(x_20, 0);
+x_34 = lean_ctor_get(x_20, 1);
+lean_inc(x_34);
 lean_inc(x_33);
-lean_inc(x_32);
-lean_dec(x_19);
-x_34 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_34, 0, x_32);
-lean_ctor_set(x_34, 1, x_33);
-return x_34;
+lean_dec(x_20);
+x_35 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_35, 0, x_33);
+lean_ctor_set(x_35, 1, x_34);
+return x_35;
 }
 }
 }
 else
 {
-uint8_t x_35; 
+uint8_t x_36; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_1);
-x_35 = !lean_is_exclusive(x_16);
-if (x_35 == 0)
+x_36 = !lean_is_exclusive(x_16);
+if (x_36 == 0)
 {
 return x_16;
 }
 else
 {
-lean_object* x_36; lean_object* x_37; lean_object* x_38; 
-x_36 = lean_ctor_get(x_16, 0);
-x_37 = lean_ctor_get(x_16, 1);
+lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_37 = lean_ctor_get(x_16, 0);
+x_38 = lean_ctor_get(x_16, 1);
+lean_inc(x_38);
 lean_inc(x_37);
-lean_inc(x_36);
 lean_dec(x_16);
-x_38 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_38, 0, x_36);
-lean_ctor_set(x_38, 1, x_37);
-return x_38;
+x_39 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_39, 0, x_37);
+lean_ctor_set(x_39, 1, x_38);
+return x_39;
 }
 }
 }
 else
 {
-uint8_t x_39; 
+uint8_t x_40; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
@@ -1019,23 +1020,23 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_39 = !lean_is_exclusive(x_9);
-if (x_39 == 0)
+x_40 = !lean_is_exclusive(x_9);
+if (x_40 == 0)
 {
 return x_9;
 }
 else
 {
-lean_object* x_40; lean_object* x_41; lean_object* x_42; 
-x_40 = lean_ctor_get(x_9, 0);
-x_41 = lean_ctor_get(x_9, 1);
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_9, 0);
+x_42 = lean_ctor_get(x_9, 1);
+lean_inc(x_42);
 lean_inc(x_41);
-lean_inc(x_40);
 lean_dec(x_9);
-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;
+x_43 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_43, 0, x_41);
+lean_ctor_set(x_43, 1, x_42);
+return x_43;
 }
 }
 }

stage0/stdlib/Lean/Server/Watchdog.c

@@ -27,7 +27,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_forwardNotification___rarg(lean_
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startFileWorker(lean_object*, lean_object*, lean_object*);
 size_t lean_usize_add(size_t, size_t);
 lean_object* lean_get_stdout(lean_object*);
-static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__3;
+LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__52;
 extern lean_object* l_String_instInhabitedString;
 static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__10;
@@ -86,6 +86,7 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__56;
 LEAN_EXPORT lean_object* l_Std_RBNode_erase___at_Lean_Server_Watchdog_eraseFileWorker___spec__1___boxed(lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_initAndRunWatchdog___closed__9;
+lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_searchPathRef;
 static lean_object* l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_findDefinitions___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -102,6 +103,8 @@ lean_object* l_Lean_Lsp_DocumentUri_toPath_x3f(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__12(lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__4___boxed(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__2;
 lean_object* lean_private_to_user_name(lean_object*);
 static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__53;
@@ -356,7 +359,6 @@ static lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_handleCan
 static lean_object* l_Lean_Server_Watchdog_handleDidChangeWatchedFiles___closed__2;
 static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__6;
 static lean_object* l_Lean_Server_Watchdog_findWorkerPath___lambda__2___closed__1;
-static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__2;
 static lean_object* l_IO_FS_Stream_readLspNotificationAs___at_Lean_Server_Watchdog_initAndRunWatchdogAux___spec__1___closed__1;
 static lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_handleCancelRequest___spec__3___closed__1;
 lean_object* lean_int_neg(lean_object*);
@@ -371,6 +373,7 @@ LEAN_EXPORT lean_object* l_Std_RBNode_del___at_Lean_Server_Watchdog_eraseFileWor
 static lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop___closed__2;
 static lean_object* l_Lean_Server_Watchdog_findWorkerPath___lambda__2___closed__2;
 static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__1;
+static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__2;
 static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__9;
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_shutdown(lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__4;
@@ -387,6 +390,7 @@ lean_object* l_Lean_Json_opt___at_Lean_JsonRpc_instToJsonMessage___spec__2(lean_
 static lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop___closed__12;
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_tryWriteMessage___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_initAndRunWatchdog(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_String_isEmpty(lean_object*);
 lean_object* lean_io_getenv(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_parseHeaderAst___closed__1;
 lean_object* l_Lean_FuzzyMatching_fuzzyMatchScoreWithThreshold_x3f(lean_object*, lean_object*, double);
@@ -511,7 +515,6 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleCancelRequest(lean_object*
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_tryWriteMessage___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_initAndRunWatchdog___closed__14;
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_log(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__1;
 LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_Server_Watchdog_updateFileWorkers___spec__2(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__12___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_initAndRunWatchdog___closed__3;
@@ -8776,17 +8779,7 @@ return x_26;
 }
 }
 }
-static lean_object* _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__1() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = lean_unsigned_to_nat(100u);
-x_2 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
-}
-}
-static lean_object* _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__2() {
+static lean_object* _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -8798,11 +8791,11 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__3() {
+static lean_object* _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__2;
+x_1 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__1;
 x_2 = l_Lean_Lsp_instInhabitedLocation;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
@@ -8810,98 +8803,127 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_5 = lean_ctor_get(x_3, 9);
+lean_inc(x_5);
+x_6 = lean_st_ref_get(x_5, x_4);
+lean_dec(x_5);
+x_7 = lean_ctor_get(x_6, 0);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_6, 1);
+lean_inc(x_8);
+lean_dec(x_6);
+x_9 = lean_ctor_get(x_3, 8);
+lean_inc(x_9);
+lean_dec(x_3);
+x_10 = lean_alloc_closure((void*)(l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1), 2, 1);
+lean_closure_set(x_10, 0, x_1);
+x_11 = lean_box(0);
+x_12 = l_Lean_Server_References_definitionsMatching___rarg(x_7, x_9, x_10, x_11, x_8);
+if (lean_obj_tag(x_12) == 0)
+{
+uint8_t x_13; 
+x_13 = !lean_is_exclusive(x_12);
+if (x_13 == 0)
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; size_t x_24; size_t x_25; lean_object* x_26; 
+x_14 = lean_ctor_get(x_12, 0);
+x_15 = lean_array_get_size(x_14);
+x_16 = lean_unsigned_to_nat(1u);
+x_17 = lean_nat_sub(x_15, x_16);
+lean_dec(x_15);
+x_18 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__2;
+x_19 = lean_unsigned_to_nat(0u);
+x_20 = l_Array_qsort_sort___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__1(x_18, x_14, x_19, x_17);
+lean_dec(x_17);
+x_21 = lean_unsigned_to_nat(100u);
+x_22 = l_Array_extract___rarg(x_20, x_19, x_21);
+x_23 = lean_array_get_size(x_22);
+x_24 = lean_usize_of_nat(x_23);
+lean_dec(x_23);
+x_25 = 0;
+x_26 = l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__2(x_24, x_25, x_22);
+lean_ctor_set(x_12, 0, x_26);
+return x_12;
+}
+else
+{
+lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; size_t x_38; size_t x_39; lean_object* x_40; lean_object* x_41; 
+x_27 = lean_ctor_get(x_12, 0);
+x_28 = lean_ctor_get(x_12, 1);
+lean_inc(x_28);
+lean_inc(x_27);
+lean_dec(x_12);
+x_29 = lean_array_get_size(x_27);
+x_30 = lean_unsigned_to_nat(1u);
+x_31 = lean_nat_sub(x_29, x_30);
+lean_dec(x_29);
+x_32 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__2;
+x_33 = lean_unsigned_to_nat(0u);
+x_34 = l_Array_qsort_sort___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__1(x_32, x_27, x_33, x_31);
+lean_dec(x_31);
+x_35 = lean_unsigned_to_nat(100u);
+x_36 = l_Array_extract___rarg(x_34, x_33, x_35);
+x_37 = lean_array_get_size(x_36);
+x_38 = lean_usize_of_nat(x_37);
+lean_dec(x_37);
+x_39 = 0;
+x_40 = l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__2(x_38, x_39, x_36);
+x_41 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_41, 0, x_40);
+lean_ctor_set(x_41, 1, x_28);
+return x_41;
+}
+}
+else
+{
+uint8_t x_42; 
+x_42 = !lean_is_exclusive(x_12);
+if (x_42 == 0)
+{
+return x_12;
+}
+else
+{
+lean_object* x_43; lean_object* x_44; lean_object* x_45; 
+x_43 = lean_ctor_get(x_12, 0);
+x_44 = lean_ctor_get(x_12, 1);
+lean_inc(x_44);
+lean_inc(x_43);
+lean_dec(x_12);
+x_45 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_45, 0, x_43);
+lean_ctor_set(x_45, 1, x_44);
+return x_45;
+}
+}
+}
+}
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_4 = lean_ctor_get(x_2, 9);
-lean_inc(x_4);
-x_5 = lean_st_ref_get(x_4, x_3);
-lean_dec(x_4);
-x_6 = lean_ctor_get(x_5, 0);
-lean_inc(x_6);
-x_7 = lean_ctor_get(x_5, 1);
-lean_inc(x_7);
-lean_dec(x_5);
-x_8 = lean_ctor_get(x_2, 8);
-lean_inc(x_8);
+uint8_t x_4; 
+x_4 = l_String_isEmpty(x_1);
+if (x_4 == 0)
+{
+lean_object* x_5; lean_object* x_6; 
+x_5 = lean_box(0);
+x_6 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2(x_1, x_5, x_2, x_3);
+return x_6;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; 
 lean_dec(x_2);
-x_9 = lean_alloc_closure((void*)(l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1), 2, 1);
-lean_closure_set(x_9, 0, x_1);
-x_10 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__1;
-x_11 = l_Lean_Server_References_definitionsMatching___rarg(x_6, x_8, x_9, x_10, x_7);
-if (lean_obj_tag(x_11) == 0)
-{
-uint8_t x_12; 
-x_12 = !lean_is_exclusive(x_11);
-if (x_12 == 0)
-{
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; size_t x_21; size_t x_22; lean_object* x_23; 
-x_13 = lean_ctor_get(x_11, 0);
-x_14 = lean_array_get_size(x_13);
-x_15 = lean_unsigned_to_nat(1u);
-x_16 = lean_nat_sub(x_14, x_15);
-lean_dec(x_14);
-x_17 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__3;
-x_18 = lean_unsigned_to_nat(0u);
-x_19 = l_Array_qsort_sort___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__1(x_17, x_13, x_18, x_16);
-lean_dec(x_16);
-x_20 = lean_array_get_size(x_19);
-x_21 = lean_usize_of_nat(x_20);
-lean_dec(x_20);
-x_22 = 0;
-x_23 = l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__2(x_21, x_22, x_19);
-lean_ctor_set(x_11, 0, x_23);
-return x_11;
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; size_t x_33; size_t x_34; lean_object* x_35; lean_object* x_36; 
-x_24 = lean_ctor_get(x_11, 0);
-x_25 = lean_ctor_get(x_11, 1);
-lean_inc(x_25);
-lean_inc(x_24);
-lean_dec(x_11);
-x_26 = lean_array_get_size(x_24);
-x_27 = lean_unsigned_to_nat(1u);
-x_28 = lean_nat_sub(x_26, x_27);
-lean_dec(x_26);
-x_29 = l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__3;
-x_30 = lean_unsigned_to_nat(0u);
-x_31 = l_Array_qsort_sort___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__1(x_29, x_24, x_30, x_28);
-lean_dec(x_28);
-x_32 = lean_array_get_size(x_31);
-x_33 = lean_usize_of_nat(x_32);
-lean_dec(x_32);
-x_34 = 0;
-x_35 = l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__2(x_33, x_34, x_31);
-x_36 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_36, 0, x_35);
-lean_ctor_set(x_36, 1, x_25);
-return x_36;
-}
-}
-else
-{
-uint8_t x_37; 
-x_37 = !lean_is_exclusive(x_11);
-if (x_37 == 0)
-{
-return x_11;
-}
-else
-{
-lean_object* x_38; lean_object* x_39; lean_object* x_40; 
-x_38 = lean_ctor_get(x_11, 0);
-x_39 = lean_ctor_get(x_11, 1);
-lean_inc(x_39);
-lean_inc(x_38);
-lean_dec(x_11);
-x_40 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_40, 0, x_38);
-lean_ctor_set(x_40, 1, x_39);
-return x_40;
-}
+lean_dec(x_1);
+x_7 = l_Lean_Server_Watchdog_startFileWorker___closed__4;
+x_8 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_8, 0, x_7);
+lean_ctor_set(x_8, 1, x_3);
+return x_8;
 }
 }
 }
@@ -8935,6 +8957,15 @@ x_6 = l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___s
 return x_6;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___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_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2(x_1, x_2, x_3, x_4);
+lean_dec(x_2);
+return x_5;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleDidOpen(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -23747,12 +23778,10 @@ lean_mark_persistent(l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___
 l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__11 = _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__11();
 lean_mark_persistent(l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__11);
 l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__12 = _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__12();
-l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__1 = _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__1();
-lean_mark_persistent(l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__1);
-l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__2 = _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__2();
-lean_mark_persistent(l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__2);
-l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__3 = _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__3();
-lean_mark_persistent(l_Lean_Server_Watchdog_handleWorkspaceSymbol___closed__3);
+l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__1 = _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__1();
+lean_mark_persistent(l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__1);
+l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__2 = _init_l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__2();
+lean_mark_persistent(l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__2___closed__2);
 l_Lean_Server_Watchdog_handleEdits___lambda__1___closed__1 = _init_l_Lean_Server_Watchdog_handleEdits___lambda__1___closed__1();
 lean_mark_persistent(l_Lean_Server_Watchdog_handleEdits___lambda__1___closed__1);
 l_Lean_Server_Watchdog_handleEdits___closed__1 = _init_l_Lean_Server_Watchdog_handleEdits___closed__1();

stage0/stdlib/Lean/Structure.c

@@ -19,23 +19,26 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_getParentStructures
 static lean_object* l_Lean_getStructureCtor___closed__2;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__9;
 size_t lean_usize_add(size_t, size_t);
+LEAN_EXPORT lean_object* l_Lean_StructureInfo_getProjFn_x3f___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_instInhabitedStructureDescr;
-static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__6;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__24;
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* lean_nat_div(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_instInhabitedStructureInfo___closed__1;
 LEAN_EXPORT lean_object* l_Lean_StructureInfo_fieldInfo___default;
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__2___boxed(lean_object*);
 static lean_object* l_Lean_getStructureCtor___closed__4;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__15;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkDefaultFnOfProjFn___boxed(lean_object*);
 uint8_t lean_usize_dec_eq(size_t, size_t);
 lean_object* lean_array_uget(lean_object*, size_t);
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_instInhabitedStructureState;
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_getStructureInfo_x3f___spec__1(lean_object*, lean_object*);
 uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 static lean_object* l_Lean_mkDefaultFnOfProjFn___closed__1;
 size_t lean_usize_sub(size_t, size_t);
@@ -45,21 +48,21 @@ lean_object* l_Lean_Name_reprPrec(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_registerStructure(lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__2;
+LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Std_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__4;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__8;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__1;
-static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__2;
 LEAN_EXPORT lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____boxed(lean_object*, lean_object*);
 lean_object* l_Array_qpartition_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_StructureInfo_fieldNames___default;
 size_t lean_usize_shift_right(size_t, size_t);
+LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_StructureInfo_getProjFn_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__7;
 LEAN_EXPORT lean_object* l_Lean_getProjFnForField_x3f(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__27;
-static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__1;
 uint8_t lean_usize_dec_lt(size_t, size_t);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__17;
 LEAN_EXPORT lean_object* l___private_Lean_Structure_0__Lean_getStructureFieldsFlattenedAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -67,17 +70,12 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_getStructureI
 LEAN_EXPORT uint8_t l_Lean_StructureInfo_lt(lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_findField_x3f___spec__2(lean_object*, lean_object*, size_t, size_t);
 lean_object* lean_nat_add(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insert___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_getStructureInfo_x3f___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkDefaultFnOfProjFn(lean_object*);
 lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_getStructureFieldsFlattened___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_StructureFieldInfo_lt(lean_object*, lean_object*);
 size_t lean_uint64_to_usize(uint64_t);
-static size_t l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__1;
-static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__4;
 static lean_object* l_Lean_instInhabitedStructureFieldInfo___closed__1;
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Structure_0__Lean_getStructureFieldsFlattenedAux___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, size_t, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_getFieldInfo_x3f(lean_object*, lean_object*, lean_object*);
@@ -86,17 +84,18 @@ LEAN_EXPORT lean_object* l_Lean_isStructureLike___boxed(lean_object*, lean_objec
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_getParentStructures___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedConstructorVal;
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_findField_x3f___lambda__1___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_instInhabitedStructureFieldInfo;
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_getStructureInfo_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static size_t l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__1;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__2(lean_object*);
 lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
 static lean_object* l_Lean_getStructureInfo_x3f___closed__1;
 LEAN_EXPORT lean_object* l_Lean_getStructureFieldsFlattened(lean_object*, lean_object*, uint8_t);
 static lean_object* l_Lean_getStructureFields___closed__1;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__30;
+LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__5;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__18;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
@@ -105,12 +104,10 @@ static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo___
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__14;
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_getStructureInfo_x3f___spec__2(lean_object*, size_t, lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_getStructureCtor___closed__5;
 static lean_object* l_Lean_getStructureCtor___closed__3;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__28;
 uint64_t l_Lean_Name_hash(lean_object*);
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__3(lean_object*);
 LEAN_EXPORT lean_object* l_panic___at_Lean_getStructureCtor___spec__1(lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__25;
 LEAN_EXPORT lean_object* l_Lean_structureExt;
@@ -118,10 +115,11 @@ static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo___
 LEAN_EXPORT uint8_t l_Array_contains___at_Lean_findField_x3f___spec__1(lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
 static lean_object* l_Lean_StructureInfo_fieldNames___default___closed__1;
+LEAN_EXPORT lean_object* l_Lean_StructureInfo_getProjFn_x3f(lean_object*, lean_object*);
+static lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1;
 LEAN_EXPORT lean_object* l_panic___at_Lean_getStructureFields___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_getStructureFields(lean_object*, lean_object*);
 size_t lean_usize_shift_left(size_t, size_t);
-static size_t l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__2;
 uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_getStructureInfo_x3f(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__29;
@@ -131,46 +129,50 @@ LEAN_EXPORT lean_object* l_Lean_getPathToBaseStructure_x3f(lean_object*, lean_ob
 LEAN_EXPORT lean_object* l_Lean_findField_x3f___lambda__1(lean_object*, lean_object*);
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__16;
+static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__6;
 size_t lean_usize_mul(size_t, size_t);
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__2___boxed(lean_object*);
+LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_StructureInfo_getProjFn_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__3(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_registerStructure___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_findField_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_getStructureInfo_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
 size_t lean_usize_land(size_t, size_t);
 LEAN_EXPORT lean_object* l___private_Lean_Structure_0__Lean_StructureState_map___default;
-LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_getFieldInfo_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_findField_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_getAllParentStructures(lean_object*, lean_object*);
-static lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__3;
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__3(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__19;
 static lean_object* l_Lean_getStructureFields___closed__2;
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_registerStructure___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_378_(uint8_t, lean_object*);
 static lean_object* l_Lean_getStructureCtor___closed__6;
 LEAN_EXPORT lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60_(lean_object*, lean_object*);
+static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__5;
 lean_object* l_List_redLength___rarg(lean_object*);
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insert___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_contains___at_Lean_findField_x3f___spec__1___boxed(lean_object*, lean_object*);
+static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__2;
 LEAN_EXPORT lean_object* l_Lean_getParentStructures(lean_object*, lean_object*);
+static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__3;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__20;
 static lean_object* l_Array_qsort_sort___at_Lean_registerStructure___spec__2___closed__1;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 uint8_t lean_usize_dec_le(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_getDefaultFnForField_x3f(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_registerStructure___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__1;
 lean_object* l_Lean_Name_append(lean_object*, lean_object*);
 static lean_object* l_Lean_mkDefaultFnOfProjFn___closed__2;
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298_(lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__10;
 static lean_object* l___private_Lean_Structure_0__Lean_StructureState_map___default___closed__3;
-static lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1;
-LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_getStructureInfo_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__3;
 LEAN_EXPORT lean_object* l_Lean_getStructureCtor(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_isStructure___boxed(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_StructureState_map___default___closed__2;
 lean_object* l_Lean_Environment_getModuleIdxFor_x3f(lean_object*, lean_object*);
@@ -180,9 +182,11 @@ LEAN_EXPORT lean_object* l_Lean_getStructureLikeNumFields(lean_object*, lean_obj
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_getAllParentStructures_visit___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_registerStructure___spec__1(size_t, size_t, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_StructureState_map___default___closed__1;
+static size_t l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__2;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_getPathToBaseStructureAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_instInhabitedStructureInfo;
 LEAN_EXPORT lean_object* l_Lean_isSubobjectField_x3f(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__4;
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__23;
 lean_object* lean_string_length(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_findField_x3f(lean_object*, lean_object*, lean_object*);
@@ -191,23 +195,21 @@ LEAN_EXPORT lean_object* l_Lean_getPathToBaseStructureAux___boxed(lean_object*,
 static lean_object* l_Lean_findField_x3f___closed__1;
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Structure_0__Lean_getStructureFieldsFlattenedAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__21;
-LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_getFieldInfo_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__13;
 LEAN_EXPORT lean_object* l_Lean_getAllParentStructures_visit(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__11;
 LEAN_EXPORT lean_object* l_Lean_getPathToBaseStructure_x3f___boxed(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__3;
 lean_object* lean_usize_to_nat(size_t);
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__3(lean_object*);
 LEAN_EXPORT uint8_t l_Lean_isStructureLike(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_instInhabitedStructureDescr___closed__1;
 LEAN_EXPORT lean_object* l_Lean_StructureFieldInfo_lt___boxed(lean_object*, lean_object*);
-static lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__5;
 LEAN_EXPORT lean_object* l_Lean_findField_x3f___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__26;
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__1(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__2(lean_object*);
 lean_object* lean_nat_to_int(lean_object*);
 lean_object* l_Std_PersistentHashMap_mkEmptyEntries(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_findField_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Structure_0__Lean_reprStructureFieldInfo____x40_Lean_Structure___hyg_60____closed__6;
 LEAN_EXPORT lean_object* l___private_Lean_Structure_0__Lean_getStructureFieldsFlattenedAux(lean_object*, lean_object*, lean_object*, uint8_t);
@@ -796,6 +798,193 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
+LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_StructureInfo_getProjFn_x3f___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+uint8_t x_7; 
+x_7 = lean_nat_dec_le(x_5, x_6);
+if (x_7 == 0)
+{
+lean_object* x_8; 
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_1);
+x_8 = lean_box(0);
+return x_8;
+}
+else
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
+x_9 = lean_nat_add(x_5, x_6);
+x_10 = lean_unsigned_to_nat(2u);
+x_11 = lean_nat_div(x_9, x_10);
+lean_dec(x_9);
+lean_inc(x_1);
+x_12 = lean_array_get(x_1, x_3, x_11);
+x_13 = l_Lean_StructureFieldInfo_lt(x_12, x_4);
+if (x_13 == 0)
+{
+uint8_t x_14; 
+lean_dec(x_6);
+x_14 = l_Lean_StructureFieldInfo_lt(x_4, x_12);
+if (x_14 == 0)
+{
+lean_object* x_15; 
+lean_dec(x_11);
+lean_dec(x_5);
+lean_dec(x_1);
+x_15 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_15, 0, x_12);
+return x_15;
+}
+else
+{
+lean_object* x_16; uint8_t x_17; 
+lean_dec(x_12);
+x_16 = lean_unsigned_to_nat(0u);
+x_17 = lean_nat_dec_eq(x_11, x_16);
+if (x_17 == 0)
+{
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_unsigned_to_nat(1u);
+x_19 = lean_nat_sub(x_11, x_18);
+lean_dec(x_11);
+x_6 = x_19;
+goto _start;
+}
+else
+{
+lean_object* x_21; 
+lean_dec(x_11);
+lean_dec(x_5);
+lean_dec(x_1);
+x_21 = lean_box(0);
+return x_21;
+}
+}
+}
+else
+{
+lean_object* x_22; lean_object* x_23; 
+lean_dec(x_12);
+lean_dec(x_5);
+x_22 = lean_unsigned_to_nat(1u);
+x_23 = lean_nat_add(x_11, x_22);
+lean_dec(x_11);
+x_5 = x_23;
+goto _start;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_StructureInfo_getProjFn_x3f(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_3 = lean_ctor_get(x_1, 1);
+x_4 = lean_array_get_size(x_3);
+x_5 = lean_nat_dec_lt(x_2, x_4);
+lean_dec(x_4);
+if (x_5 == 0)
+{
+lean_object* x_6; 
+x_6 = lean_box(0);
+return x_6;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; uint8_t x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; 
+x_7 = lean_array_fget(x_3, x_2);
+x_8 = lean_ctor_get(x_1, 2);
+x_9 = lean_box(0);
+x_10 = lean_box(0);
+x_11 = 0;
+x_12 = 0;
+x_13 = lean_alloc_ctor(0, 3, 2);
+lean_ctor_set(x_13, 0, x_7);
+lean_ctor_set(x_13, 1, x_10);
+lean_ctor_set(x_13, 2, x_9);
+lean_ctor_set_uint8(x_13, sizeof(void*)*3, x_11);
+lean_ctor_set_uint8(x_13, sizeof(void*)*3 + 1, x_12);
+x_14 = lean_array_get_size(x_8);
+x_15 = lean_unsigned_to_nat(1u);
+x_16 = lean_nat_sub(x_14, x_15);
+x_17 = lean_unsigned_to_nat(0u);
+x_18 = lean_nat_dec_lt(x_17, x_14);
+lean_dec(x_14);
+if (x_18 == 0)
+{
+lean_object* x_19; 
+lean_dec(x_16);
+lean_dec(x_13);
+x_19 = lean_box(0);
+return x_19;
+}
+else
+{
+lean_object* x_20; lean_object* x_21; 
+x_20 = l_Lean_instInhabitedStructureFieldInfo;
+x_21 = l_Array_binSearchAux___at_Lean_StructureInfo_getProjFn_x3f___spec__1(x_20, x_9, x_8, x_13, x_17, x_16);
+lean_dec(x_13);
+if (lean_obj_tag(x_21) == 0)
+{
+lean_object* x_22; 
+x_22 = lean_box(0);
+return x_22;
+}
+else
+{
+uint8_t x_23; 
+x_23 = !lean_is_exclusive(x_21);
+if (x_23 == 0)
+{
+lean_object* x_24; lean_object* x_25; 
+x_24 = lean_ctor_get(x_21, 0);
+x_25 = lean_ctor_get(x_24, 1);
+lean_inc(x_25);
+lean_dec(x_24);
+lean_ctor_set(x_21, 0, x_25);
+return x_21;
+}
+else
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = lean_ctor_get(x_21, 0);
+lean_inc(x_26);
+lean_dec(x_21);
+x_27 = lean_ctor_get(x_26, 1);
+lean_inc(x_27);
+lean_dec(x_26);
+x_28 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_28, 0, x_27);
+return x_28;
+}
+}
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_StructureInfo_getProjFn_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Array_binSearchAux___at_Lean_StructureInfo_getProjFn_x3f___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_StructureInfo_getProjFn_x3f___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_StructureInfo_getProjFn_x3f(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
 static lean_object* _init_l___private_Lean_Structure_0__Lean_StructureState_map___default___closed__1() {
 _start:
 {
@@ -842,7 +1031,7 @@ x_1 = l___private_Lean_Structure_0__Lean_StructureState_map___default___closed__
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__3(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__3(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 lean_object* x_7; uint8_t x_8; 
@@ -869,7 +1058,7 @@ x_17 = lean_usize_shift_right(x_12, x_16);
 x_18 = lean_unsigned_to_nat(1u);
 x_19 = lean_nat_add(x_5, x_18);
 lean_dec(x_5);
-x_20 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(x_6, x_17, x_1, x_9, x_10);
+x_20 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(x_6, x_17, x_1, x_9, x_10);
 x_4 = lean_box(0);
 x_5 = x_19;
 x_6 = x_20;
@@ -877,7 +1066,7 @@ goto _start;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; 
@@ -969,7 +1158,7 @@ return x_29;
 }
 }
 }
-static size_t _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__1() {
+static size_t _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__1() {
 _start:
 {
 size_t x_1; size_t x_2; size_t x_3; 
@@ -979,17 +1168,17 @@ x_3 = lean_usize_shift_left(x_1, x_2);
 return x_3;
 }
 }
-static size_t _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__2() {
+static size_t _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__2() {
 _start:
 {
 size_t x_1; size_t x_2; size_t x_3; 
 x_1 = 1;
-x_2 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__1;
+x_2 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__1;
 x_3 = lean_usize_sub(x_2, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__3() {
+static lean_object* _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -997,7 +1186,7 @@ x_1 = l_Std_PersistentHashMap_mkEmptyEntries(lean_box(0), lean_box(0));
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5) {
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 if (lean_obj_tag(x_1) == 0)
@@ -1010,7 +1199,7 @@ lean_object* x_7; size_t x_8; size_t x_9; size_t x_10; size_t x_11; lean_object*
 x_7 = lean_ctor_get(x_1, 0);
 x_8 = 1;
 x_9 = 5;
-x_10 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__2;
+x_10 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__2;
 x_11 = lean_usize_land(x_2, x_10);
 x_12 = lean_usize_to_nat(x_11);
 x_13 = lean_array_get_size(x_7);
@@ -1110,7 +1299,7 @@ lean_object* x_35; size_t x_36; size_t x_37; lean_object* x_38; lean_object* x_3
 x_35 = lean_ctor_get(x_15, 0);
 x_36 = lean_usize_shift_right(x_2, x_9);
 x_37 = lean_usize_add(x_3, x_8);
-x_38 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(x_35, x_36, x_37, x_4, x_5);
+x_38 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(x_35, x_36, x_37, x_4, x_5);
 lean_ctor_set(x_15, 0, x_38);
 x_39 = lean_array_fset(x_17, x_12, x_15);
 lean_dec(x_12);
@@ -1125,7 +1314,7 @@ lean_inc(x_40);
 lean_dec(x_15);
 x_41 = lean_usize_shift_right(x_2, x_9);
 x_42 = lean_usize_add(x_3, x_8);
-x_43 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(x_40, x_41, x_42, x_4, x_5);
+x_43 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(x_40, x_41, x_42, x_4, x_5);
 x_44 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_44, 0, x_43);
 x_45 = lean_array_fset(x_17, x_12, x_44);
@@ -1156,7 +1345,7 @@ lean_inc(x_48);
 lean_dec(x_1);
 x_49 = 1;
 x_50 = 5;
-x_51 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__2;
+x_51 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__2;
 x_52 = lean_usize_land(x_2, x_51);
 x_53 = lean_usize_to_nat(x_52);
 x_54 = lean_array_get_size(x_48);
@@ -1241,7 +1430,7 @@ if (lean_is_exclusive(x_57)) {
 }
 x_73 = lean_usize_shift_right(x_2, x_50);
 x_74 = lean_usize_add(x_3, x_49);
-x_75 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(x_71, x_73, x_74, x_4, x_5);
+x_75 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(x_71, x_73, x_74, x_4, x_5);
 if (lean_is_scalar(x_72)) {
  x_76 = lean_alloc_ctor(1, 1, 0);
 } else {
@@ -1278,7 +1467,7 @@ if (x_82 == 0)
 {
 lean_object* x_83; lean_object* x_84; size_t x_85; uint8_t x_86; 
 x_83 = lean_unsigned_to_nat(0u);
-x_84 = l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__4(x_1, x_83, x_4, x_5);
+x_84 = l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__4(x_1, x_83, x_4, x_5);
 x_85 = 7;
 x_86 = lean_usize_dec_le(x_85, x_3);
 if (x_86 == 0)
@@ -1296,8 +1485,8 @@ lean_inc(x_90);
 x_91 = lean_ctor_get(x_84, 1);
 lean_inc(x_91);
 lean_dec(x_84);
-x_92 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__3;
-x_93 = l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__3(x_3, x_90, x_91, lean_box(0), x_83, x_92);
+x_92 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__3;
+x_93 = l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__3(x_3, x_90, x_91, lean_box(0), x_83, x_92);
 lean_dec(x_91);
 lean_dec(x_90);
 return x_93;
@@ -1324,7 +1513,7 @@ x_96 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_96, 0, x_94);
 lean_ctor_set(x_96, 1, x_95);
 x_97 = lean_unsigned_to_nat(0u);
-x_98 = l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__4(x_96, x_97, x_4, x_5);
+x_98 = l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__4(x_96, x_97, x_4, x_5);
 x_99 = 7;
 x_100 = lean_usize_dec_le(x_99, x_3);
 if (x_100 == 0)
@@ -1342,8 +1531,8 @@ lean_inc(x_104);
 x_105 = lean_ctor_get(x_98, 1);
 lean_inc(x_105);
 lean_dec(x_98);
-x_106 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__3;
-x_107 = l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__3(x_3, x_104, x_105, lean_box(0), x_97, x_106);
+x_106 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__3;
+x_107 = l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__3(x_3, x_104, x_105, lean_box(0), x_97, x_106);
 lean_dec(x_105);
 lean_dec(x_104);
 return x_107;
@@ -1361,7 +1550,7 @@ return x_98;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insert___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insert___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 uint8_t x_4; 
@@ -1374,7 +1563,7 @@ x_6 = lean_ctor_get(x_1, 1);
 x_7 = l_Lean_Name_hash(x_2);
 x_8 = lean_uint64_to_usize(x_7);
 x_9 = 1;
-x_10 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(x_5, x_8, x_9, x_2, x_3);
+x_10 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(x_5, x_8, x_9, x_2, x_3);
 x_11 = lean_unsigned_to_nat(1u);
 x_12 = lean_nat_add(x_6, x_11);
 lean_dec(x_6);
@@ -1393,7 +1582,7 @@ lean_dec(x_1);
 x_15 = l_Lean_Name_hash(x_2);
 x_16 = lean_uint64_to_usize(x_15);
 x_17 = 1;
-x_18 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(x_13, x_16, x_17, x_2, x_3);
+x_18 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(x_13, x_16, x_17, x_2, x_3);
 x_19 = lean_unsigned_to_nat(1u);
 x_20 = lean_nat_add(x_14, x_19);
 lean_dec(x_14);
@@ -1404,7 +1593,7 @@ return x_21;
 }
 }
 }
-static lean_object* _init_l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1() {
+static lean_object* _init_l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -1412,7 +1601,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_StructureInfo_lt___boxed), 2, 0);
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; uint8_t x_14; 
@@ -1469,7 +1658,7 @@ if (x_23 == 0)
 {
 lean_object* x_24; lean_object* x_25; 
 lean_dec(x_17);
-x_24 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1;
+x_24 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1;
 lean_inc_n(x_3, 2);
 lean_inc(x_1);
 x_25 = l_Array_qpartition_loop___rarg(x_1, x_24, x_4, x_19, x_18, x_3, x_3);
@@ -1484,7 +1673,7 @@ x_26 = lean_array_swap(x_18, x_17, x_4);
 lean_dec(x_17);
 lean_inc(x_1);
 x_27 = lean_array_get(x_1, x_26, x_4);
-x_28 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1;
+x_28 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1;
 lean_inc_n(x_3, 2);
 lean_inc(x_1);
 x_29 = l_Array_qpartition_loop___rarg(x_1, x_28, x_4, x_27, x_26, x_3, x_3);
@@ -1507,7 +1696,7 @@ if (x_33 == 0)
 {
 lean_object* x_34; lean_object* x_35; 
 lean_dec(x_17);
-x_34 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1;
+x_34 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1;
 lean_inc_n(x_3, 2);
 lean_inc(x_1);
 x_35 = l_Array_qpartition_loop___rarg(x_1, x_34, x_4, x_32, x_30, x_3, x_3);
@@ -1522,7 +1711,7 @@ x_36 = lean_array_swap(x_30, x_17, x_4);
 lean_dec(x_17);
 lean_inc(x_1);
 x_37 = lean_array_get(x_1, x_36, x_4);
-x_38 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1;
+x_38 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1;
 lean_inc_n(x_3, 2);
 lean_inc(x_1);
 x_39 = l_Array_qpartition_loop___rarg(x_1, x_38, x_4, x_37, x_36, x_3, x_3);
@@ -1545,7 +1734,7 @@ if (x_8 == 0)
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; 
 lean_inc(x_1);
-x_9 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5(x_1, x_7, x_3, x_6);
+x_9 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5(x_1, x_7, x_3, x_6);
 x_10 = lean_unsigned_to_nat(1u);
 x_11 = lean_nat_add(x_6, x_10);
 lean_dec(x_6);
@@ -1563,17 +1752,17 @@ return x_7;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__1(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
-x_4 = l_Std_PersistentHashMap_insert___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__1(x_1, x_3, x_2);
+x_4 = l_Std_PersistentHashMap_insert___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__1(x_1, x_3, x_2);
 return x_4;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__2(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__2(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
@@ -1581,7 +1770,7 @@ x_2 = l___private_Lean_Structure_0__Lean_StructureState_map___default___closed__
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__3(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__3(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
@@ -1595,12 +1784,12 @@ x_7 = lean_nat_sub(x_5, x_6);
 lean_dec(x_5);
 x_8 = l_Lean_instInhabitedStructureInfo;
 x_9 = lean_unsigned_to_nat(0u);
-x_10 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5(x_8, x_4, x_9, x_7);
+x_10 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5(x_8, x_4, x_9, x_7);
 lean_dec(x_7);
 return x_10;
 }
 }
-static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__1() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -1608,48 +1797,48 @@ x_1 = lean_mk_string("structExt");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__2() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__1;
+x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__3() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__3() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__1), 2, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__1), 2, 0);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__4() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__4() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__2___boxed), 1, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__2___boxed), 1, 0);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__5() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__5() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__3), 1, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__3), 1, 0);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__6() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__2;
-x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__3;
-x_3 = l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__4;
-x_4 = l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__5;
+x_1 = l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__2;
+x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__3;
+x_3 = l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__4;
+x_4 = l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__5;
 x_5 = lean_alloc_ctor(0, 4, 0);
 lean_ctor_set(x_5, 0, x_1);
 lean_ctor_set(x_5, 1, x_2);
@@ -1658,28 +1847,28 @@ lean_ctor_set(x_5, 3, x_4);
 return x_5;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__6;
+x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__6;
 x_3 = l_Lean_registerSimplePersistentEnvExtension___rarg(x_2, x_1);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 size_t x_7; lean_object* x_8; 
 x_7 = lean_unbox_usize(x_1);
 lean_dec(x_1);
-x_8 = l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__3(x_7, x_2, x_3, x_4, x_5, x_6);
+x_8 = l_Std_PersistentHashMap_insertAux_traverse___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__3(x_7, x_2, x_3, x_4, x_5, x_6);
 lean_dec(x_3);
 lean_dec(x_2);
 return x_8;
 }
 }
-LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 size_t x_6; size_t x_7; lean_object* x_8; 
@@ -1687,24 +1876,24 @@ x_6 = lean_unbox_usize(x_2);
 lean_dec(x_2);
 x_7 = lean_unbox_usize(x_3);
 lean_dec(x_3);
-x_8 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2(x_1, x_6, x_7, x_4, x_5);
+x_8 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2(x_1, x_6, x_7, x_4, x_5);
 return x_8;
 }
 }
-LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___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_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5(x_1, x_2, x_3, x_4);
+x_5 = l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5(x_1, x_2, x_3, x_4);
 lean_dec(x_4);
 return x_5;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__2___boxed(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__2___boxed(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_241____lambda__2(x_1);
+x_2 = l_Lean_initFn____x40_Lean_Structure___hyg_298____lambda__2(x_1);
 lean_dec(x_1);
 return x_2;
 }
@@ -2026,7 +2215,7 @@ x_4 = lean_ctor_get(x_1, 0);
 lean_inc(x_4);
 lean_dec(x_1);
 x_5 = 5;
-x_6 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__2;
+x_6 = l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__2;
 x_7 = lean_usize_land(x_2, x_6);
 x_8 = lean_usize_to_nat(x_7);
 x_9 = lean_box(2);
@@ -2332,7 +2521,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_getStructureCtor___closed__1;
 x_2 = l_Lean_getStructureCtor___closed__2;
-x_3 = lean_unsigned_to_nat(68u);
+x_3 = lean_unsigned_to_nat(75u);
 x_4 = lean_unsigned_to_nat(9u);
 x_5 = l_Lean_getStructureCtor___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -2353,7 +2542,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_getStructureCtor___closed__1;
 x_2 = l_Lean_getStructureCtor___closed__2;
-x_3 = lean_unsigned_to_nat(67u);
+x_3 = lean_unsigned_to_nat(74u);
 x_4 = lean_unsigned_to_nat(11u);
 x_5 = l_Lean_getStructureCtor___closed__5;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -2503,7 +2692,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_getStructureCtor___closed__1;
 x_2 = l_Lean_getStructureFields___closed__1;
-x_3 = lean_unsigned_to_nat(75u);
+x_3 = lean_unsigned_to_nat(82u);
 x_4 = lean_unsigned_to_nat(4u);
 x_5 = l_Lean_getStructureCtor___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -2535,85 +2724,6 @@ return x_7;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_getFieldInfo_x3f___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-uint8_t x_7; 
-x_7 = lean_nat_dec_le(x_5, x_6);
-if (x_7 == 0)
-{
-lean_object* x_8; 
-lean_dec(x_6);
-lean_dec(x_5);
-lean_dec(x_1);
-x_8 = lean_box(0);
-return x_8;
-}
-else
-{
-lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_9 = lean_nat_add(x_5, x_6);
-x_10 = lean_unsigned_to_nat(2u);
-x_11 = lean_nat_div(x_9, x_10);
-lean_dec(x_9);
-lean_inc(x_1);
-x_12 = lean_array_get(x_1, x_3, x_11);
-x_13 = l_Lean_StructureFieldInfo_lt(x_12, x_4);
-if (x_13 == 0)
-{
-uint8_t x_14; 
-lean_dec(x_6);
-x_14 = l_Lean_StructureFieldInfo_lt(x_4, x_12);
-if (x_14 == 0)
-{
-lean_object* x_15; 
-lean_dec(x_11);
-lean_dec(x_5);
-lean_dec(x_1);
-x_15 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_15, 0, x_12);
-return x_15;
-}
-else
-{
-lean_object* x_16; uint8_t x_17; 
-lean_dec(x_12);
-x_16 = lean_unsigned_to_nat(0u);
-x_17 = lean_nat_dec_eq(x_11, x_16);
-if (x_17 == 0)
-{
-lean_object* x_18; lean_object* x_19; 
-x_18 = lean_unsigned_to_nat(1u);
-x_19 = lean_nat_sub(x_11, x_18);
-lean_dec(x_11);
-x_6 = x_19;
-goto _start;
-}
-else
-{
-lean_object* x_21; 
-lean_dec(x_11);
-lean_dec(x_5);
-lean_dec(x_1);
-x_21 = lean_box(0);
-return x_21;
-}
-}
-}
-else
-{
-lean_object* x_22; lean_object* x_23; 
-lean_dec(x_12);
-lean_dec(x_5);
-x_22 = lean_unsigned_to_nat(1u);
-x_23 = lean_nat_add(x_11, x_22);
-lean_dec(x_11);
-x_5 = x_23;
-goto _start;
-}
-}
-}
-}
 LEAN_EXPORT lean_object* l_Lean_getFieldInfo_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -2664,7 +2774,7 @@ else
 {
 lean_object* x_19; lean_object* x_20; 
 x_19 = l_Lean_instInhabitedStructureFieldInfo;
-x_20 = l_Array_binSearchAux___at_Lean_getFieldInfo_x3f___spec__1(x_19, x_8, x_7, x_12, x_16, x_15);
+x_20 = l_Array_binSearchAux___at_Lean_StructureInfo_getProjFn_x3f___spec__1(x_19, x_8, x_7, x_12, x_16, x_15);
 lean_dec(x_12);
 lean_dec(x_7);
 return x_20;
@@ -2672,17 +2782,6 @@ return x_20;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Lean_getFieldInfo_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-lean_object* x_7; 
-x_7 = l_Array_binSearchAux___at_Lean_getFieldInfo_x3f___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
-lean_dec(x_4);
-lean_dec(x_3);
-lean_dec(x_2);
-return x_7;
-}
-}
 LEAN_EXPORT lean_object* l_Lean_isSubobjectField_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -4068,25 +4167,25 @@ l___private_Lean_Structure_0__Lean_StructureState_map___default = _init_l___priv
 lean_mark_persistent(l___private_Lean_Structure_0__Lean_StructureState_map___default);
 l_Lean_instInhabitedStructureState = _init_l_Lean_instInhabitedStructureState();
 lean_mark_persistent(l_Lean_instInhabitedStructureState);
-l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__1 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__1();
-l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__2 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__2();
-l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__3 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__3();
-lean_mark_persistent(l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__2___closed__3);
-l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1 = _init_l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1();
-lean_mark_persistent(l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_241____spec__5___closed__1);
-l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__1 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__1();
-lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__1);
-l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__2 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__2();
-lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__2);
-l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__3 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__3();
-lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__3);
-l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__4 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__4();
-lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__4);
-l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__5 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__5();
-lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__5);
-l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__6 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__6();
-lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_241____closed__6);
-if (builtin) {res = l_Lean_initFn____x40_Lean_Structure___hyg_241_(lean_io_mk_world());
+l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__1 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__1();
+l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__2 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__2();
+l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__3 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__3();
+lean_mark_persistent(l_Std_PersistentHashMap_insertAux___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__2___closed__3);
+l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1 = _init_l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1();
+lean_mark_persistent(l_Array_qsort_sort___at_Lean_initFn____x40_Lean_Structure___hyg_298____spec__5___closed__1);
+l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__1 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__1();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__1);
+l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__2 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__2();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__2);
+l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__3 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__3();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__3);
+l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__4 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__4();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__4);
+l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__5 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__5();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__5);
+l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__6 = _init_l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__6();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Structure___hyg_298____closed__6);
+if (builtin) {res = l_Lean_initFn____x40_Lean_Structure___hyg_298_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 l_Lean_structureExt = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_structureExt);