chore: update stage0

stage0/src/Init/Control/Basic.lean

@@ -228,3 +228,21 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂))
   forM [Monad m] : γ → (α → m PUnit) → m PUnit
 
 export ForM (forM)
+
+/-- Left-to-right composition of Kleisli arrows. -/
+def Bind.kleisliRight [Bind m] (f₁ : α → m β) (f₂ : β → m γ) (a : α) : m γ :=
+  f₁ a >>= f₂
+
+/-- Right-to-left composition of Kleisli arrows. -/
+def Bind.kleisliLeft [Bind m] (f₂ : β → m γ) (f₁ : α → m β) (a : α) : m γ :=
+  f₁ a >>= f₂
+
+/-- Same as `Bind.bind` but with arguments swapped. -/
+def Bind.bindLeft [Bind m] (f : α → m β) (ma : m α) : m β :=
+  ma >>= f
+
+-- Precedence choice taken to be the same as in haskell:
+-- https://hackage.haskell.org/package/base-4.17.0.0/docs/Control-Monad.html#v:-61--60--60-
+@[inheritDoc] infixr:55 " >=> " => Bind.kleisliRight
+@[inheritDoc] infixr:55 " <=< " => Bind.kleisliLeft
+@[inheritDoc] infixr:55 " =<< " => Bind.bindLeft

stage0/src/Lean/Compiler/LCNF/Bind.lean

@@ -66,21 +66,29 @@ where
       else
         return ps
 
-def etaExpandCore? (type : Expr) (params : Array Param) (value : Code) : CompilerM (Option (Array Param × Code)) := do
+def isEtaExpandCandidateCore (type : Expr) (params : Array Param) : Bool :=
   let typeArity := getArrowArity type
   let valueArity := params.size
-  if typeArity <= valueArity then
-    -- It can be < because of the "any" type
-    return none
+  typeArity > valueArity
+
+abbrev FunDeclCore.isEtaExpandCandidate (decl : FunDecl) : Bool :=
+  isEtaExpandCandidateCore decl.type decl.params
+
+def etaExpandCore (type : Expr) (params : Array Param) (value : Code) : CompilerM (Array Param × Code) := do
+  let valueType ← instantiateForall type params
+  let psNew ← mkNewParams valueType
+  let params := params ++ psNew
+  let xs := psNew.map fun p => Expr.fvar p.fvarId
+  let value ← value.bind fun fvarId => do
+    let auxDecl ← mkAuxLetDecl (mkAppN (.fvar fvarId) xs)
+    return .let auxDecl (.return auxDecl.fvarId)
+  return (params, value)
+
+def etaExpandCore? (type : Expr) (params : Array Param) (value : Code) : CompilerM (Option (Array Param × Code)) := do
+  if isEtaExpandCandidateCore type params then
+    etaExpandCore type params value
   else
-    let valueType ← instantiateForall type params
-    let psNew ← mkNewParams valueType
-    let params := params ++ psNew
-    let xs := psNew.map fun p => Expr.fvar p.fvarId
-    let value ← value.bind fun fvarId => do
-      let auxDecl ← mkAuxLetDecl (mkAppN (.fvar fvarId) xs)
-      return .let auxDecl (.return auxDecl.fvarId)
-    return (params, value)
+    return none
 
 def FunDeclCore.etaExpand (decl : FunDecl) : CompilerM FunDecl := do
   let some (params, value) ← etaExpandCore? decl.type decl.params decl.value | return decl

stage0/src/Lean/Compiler/LCNF/CompilerM.lean

@@ -162,50 +162,49 @@ private def refreshBinderName (binderName : Name) : CompilerM Name := do
 
 namespace Internalize
 
-abbrev M := StateRefT FVarSubst CompilerM
+abbrev InternalizeM := StateRefT FVarSubst CompilerM
 
-instance : MonadFVarSubst M where
+instance : MonadFVarSubst InternalizeM where
   getSubst := get
 
-private def mkNewFVarId (fvarId : FVarId) : M FVarId := do
+private def mkNewFVarId (fvarId : FVarId) : InternalizeM FVarId := do
   let fvarId' ← Lean.mkFreshFVarId
   modify fun s => s.insert fvarId (.fvar fvarId')
   return fvarId'
 
-private def addParam (p : Param) : M Param := do
+def internalizeParam (p : Param) : InternalizeM Param := do
   let type ← normExpr p.type
   let fvarId ← mkNewFVarId p.fvarId
   let p := { p with fvarId, type }
   modifyLCtx fun lctx => lctx.addParam p
   return p
 
+def internalizeLetDecl (decl : LetDecl) : InternalizeM LetDecl := do
+  let binderName ← refreshBinderName decl.binderName
+  let type ← normExpr decl.type
+  let value ← normExpr decl.value
+  let fvarId ← mkNewFVarId decl.fvarId
+  let decl := { decl with binderName, fvarId, type, value }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  return decl
+
 mutual
 
-partial def internalizeFunDecl (decl : FunDecl) : M FunDecl := do
+partial def internalizeFunDecl (decl : FunDecl) : InternalizeM FunDecl := do
   let type ← normExpr decl.type
   let binderName ← refreshBinderName decl.binderName
-  let params ← decl.params.mapM addParam
+  let params ← decl.params.mapM internalizeParam
   let value ← internalizeCode decl.value
   let fvarId ← mkNewFVarId decl.fvarId
   let decl := { decl with binderName, fvarId, params, type, value }
   modifyLCtx fun lctx => lctx.addFunDecl decl
   return decl
 
-partial def internalizeCode (code : Code) : M Code := do
+partial def internalizeCode (code : Code) : InternalizeM Code := do
   match code with
-  | .let decl k =>
-    let binderName ← refreshBinderName decl.binderName
-    let type ← normExpr decl.type
-    let value ← normExpr decl.value
-    let fvarId ← mkNewFVarId decl.fvarId
-    let decl := { decl with binderName, fvarId, type, value }
-    modifyLCtx fun lctx => lctx.addLetDecl decl
-    let k ← internalizeCode k
-    return .let decl k
-  | .fun decl k =>
-    return .fun (← internalizeFunDecl decl) (← internalizeCode k)
-  | .jp decl k =>
-    return .jp (← internalizeFunDecl decl) (← internalizeCode k)
+  | .let decl k => return .let (← internalizeLetDecl decl) (← internalizeCode k)
+  | .fun decl k => return .fun (← internalizeFunDecl decl) (← internalizeCode k)
+  | .jp decl k => return .jp (← internalizeFunDecl decl) (← internalizeCode k)
   | .return fvarId => return .return (← normFVar fvarId)
   | .jmp fvarId args => return .jmp (← normFVar fvarId) (← args.mapM normExpr)
   | .unreach type => return .unreach (← normExpr type)
@@ -213,12 +212,18 @@ partial def internalizeCode (code : Code) : M Code := do
     let resultType ← normExpr c.resultType
     let discr ← normFVar c.discr
     let alts ← c.alts.mapM fun
-      | .alt ctorName params k => return .alt ctorName (← params.mapM addParam) (← internalizeCode k)
+      | .alt ctorName params k => return .alt ctorName (← params.mapM internalizeParam) (← internalizeCode k)
       | .default k => return .default (← internalizeCode k)
     return .cases { c with discr, alts, resultType }
 
 end
 
+partial def internalizeCodeDecl (decl : CodeDecl) : InternalizeM CodeDecl := do
+  match decl with
+  | .let decl => return .let (← internalizeLetDecl decl)
+  | .fun decl => return .fun (← internalizeFunDecl decl)
+  | .jp decl => return .jp (← internalizeFunDecl decl)
+
 end Internalize
 
 /--
@@ -231,9 +236,9 @@ open Internalize in
 def Decl.internalize (decl : Decl) (s : FVarSubst := {}): CompilerM Decl :=
   go decl |>.run' s
 where
-  go (decl : Decl) : M Decl := do
+  go (decl : Decl) : InternalizeM Decl := do
     let type ← normExpr decl.type
-    let params ← decl.params.mapM addParam
+    let params ← decl.params.mapM internalizeParam
     let value ← internalizeCode decl.value
     return { decl with type, params, value }
 

stage0/src/Lean/Compiler/LCNF/InferType.lean

@@ -221,7 +221,7 @@ where
   go (type : Expr) (i : Nat) : CoreM Expr :=
     if h : i < params.size then
       let p := params[i]
-      match type with
+      match type.headBeta with
       | .forallE _ _ b _ => go (b.instantiate1 (.fvar p.fvarId)) (i+1)
       | _ => throwError "invalid instantiateForall, too many parameters"
     else

stage0/src/Lean/Compiler/LCNF/Level.lean

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Util.CollectLevelParams
+import Lean.Compiler.LCNF.Basic
+
+namespace Lean.Compiler.LCNF
+
+/-!
+# Universe level utilities for the code generator
+-/
+
+namespace NormLevelParam
+open Std
+
+/-!
+## Universe level parameter normalizer
+
+The specializer creates "keys" for a function specialization. The key is an expression
+containing the function being specialized and the argument values used for the specialization.
+The key does not contain free variables, and function parameter names are irrelevant due to alpha
+equivalence. The universe level normalizer ensures the universe parameter names are irrelevant
+when comparing keys.
+-/
+
+/-- State for the universe level normalizer monad. -/
+structure State where
+  /-- Counter for generating new (normalized) universe parameter names. -/
+  nextIdx    : Nat := 1
+  /-- Mapping from existing universe parameter names to the new ones. -/
+  map        : HashMap Name Level := {}
+  /-- Parameters that have been normalized. -/
+  paramNames : Array Name := #[]
+
+/-- Monad for the universe leve normalizer -/
+abbrev M := StateM State
+
+/--
+Normalize universe level parameter names in the given universe level.
+-/
+partial def normLevel (u : Level) : M Level := do
+  if !u.hasParam then
+    return u
+  else match u with
+    | .zero     => return u
+    | .succ v   => return u.updateSucc! (← normLevel v)
+    | .max v w  => return u.updateMax! (← normLevel v) (← normLevel w)
+    | .imax v w => return u.updateIMax! (← normLevel v) (← normLevel w)
+    | .mvar _   => unreachable!
+    | .param n  => match (← get).map.find? n with
+      | some u => return u
+      | none   =>
+        let u := Level.param <| (`u).appendIndexAfter (← get).nextIdx
+        modify fun { nextIdx, map, paramNames } =>
+          { nextIdx := nextIdx + 1, map := map.insert n u, paramNames := paramNames.push n }
+        return u
+
+/--
+Normalize universe level parameter names in the given expression.
+-/
+partial def normExpr (e : Expr) : M Expr := do
+  if !e.hasLevelParam then
+    return e
+  else match e with
+    | .const _ us      => return e.updateConst! (← us.mapM normLevel)
+    | .sort u          => return e.updateSort! (← normLevel u)
+    | .app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
+    | .letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
+    | .forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
+    | .lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
+    | .mdata _ b       => return e.updateMData! (← normExpr b)
+    | .proj _ _ b      => return e.updateProj! (← normExpr b)
+    | .mvar _          => unreachable!
+    | _                => return e
+
+end NormLevelParam
+
+/--
+Normalize universe level parameter names in the given expression.
+The function also returns the list of universe level parameter names that have been normalized.
+-/
+def normLevelParams (e : Expr) : Expr × List Name :=
+  let (e, s) := NormLevelParam.normExpr e |>.run {}
+  (e, s.paramNames.toList)
+
+namespace CollectLevelParams
+/-!
+## Universe level collector
+
+This module extends support for `Code`. See `Lean.Util.CollectLevelParams.lean`
+
+In the code specializer, we create new auxiliary declarations and the
+universe level parameter collector is used to setup the new auxiliary declarations.
+
+See `Decl.setLevelParams`.
+-/
+open Lean.CollectLevelParams
+
+def visitParam (p : Param) : Visitor :=
+  visitExpr p.type
+
+def visitParams (ps : Array Param) : Visitor :=
+  fun s => ps.foldl (init := s) fun s p => visitParam p s
+
+mutual
+  partial def visitAlt (alt : Alt) : Visitor :=
+    match alt with
+    | .default k => visitCode k
+    | .alt _ ps k => visitCode k ∘ visitParams ps
+
+  partial def visitAlts (alts : Array Alt) : Visitor :=
+    fun s => alts.foldl (init := s) fun s alt => visitAlt alt s
+
+  partial def visitCode : Code → Visitor
+    | .let decl k => visitCode k ∘ visitExpr decl.value ∘ visitExpr decl.type
+    | .fun decl k | .jp decl k => visitCode k ∘ visitCode decl.value ∘ visitParams decl.params ∘ visitExpr decl.type
+    | .cases c => visitAlts c.alts ∘ visitExpr c.resultType
+    | .unreach type => visitExpr type
+    | .return _ => id
+    | .jmp _ args => fun s => args.foldl (init := s) fun s arg => visitExpr arg s
+end
+
+end CollectLevelParams
+
+open Lean.CollectLevelParams
+open CollectLevelParams
+
+/--
+Collect universe level parameters collecting in the type, parameters, and value, and then
+set `decl.levelParams` with the resulting value.
+-/
+def Decl.setLevelParams (decl : Decl) : Decl :=
+  let levelParams := (visitCode decl.value ∘ visitParams decl.params ∘ visitExpr decl.type) {} |>.params.toList
+  { decl with levelParams }
+
+end Lean.Compiler.LCNF

stage0/src/Lean/Compiler/LCNF/PassManager.lean

@@ -30,11 +30,11 @@ on the `Decl`s as well as meta information.
 -/
 structure Pass where
   /--
-  Which occurence of the pass in the pipeline this is.
+  Which occurrence of the pass in the pipeline this is.
   Some passes, like simp, can occur multiple times in the pipeline.
   For most passes this value does not matter.
   -/
-  occurence : Nat := 0
+  occurrence : Nat := 0
   /--
   Which phase this `Pass` is supposed to run in
   -/
@@ -96,8 +96,8 @@ end Phase
 
 namespace Pass
 
-def mkPerDeclaration (name : Name) (run : Decl → CompilerM Decl) (phase : Phase) (occurence : Nat := 0) : Pass where
-  occurence := occurence
+def mkPerDeclaration (name : Name) (run : Decl → CompilerM Decl) (phase : Phase) (occurrence : Nat := 0) : Pass where
+  occurrence := occurrence
   phase := phase
   name := name
   run := fun xs => xs.mapM run
@@ -113,12 +113,12 @@ def validate (manager : PassManager) : CompilerM Unit := do
       throwError s!"{pass.name} has phase {pass.phase} but should at least have {current}"
     current := pass.phase
 
-def findHighestOccurence (targetName : Name) (passes : Array Pass) : CompilerM Nat := do
+def findHighestOccurrence (targetName : Name) (passes : Array Pass) : CompilerM Nat := do
   let mut highest := none
   for pass in passes do
       if pass.name == targetName then
-        highest := some pass.occurence
-  let some val := highest | throwError s!"Could not find any occurence of {targetName}"
+        highest := some pass.occurrence
+  let some val := highest | throwError s!"Could not find any occurrence of {targetName}"
   return val
 
 end PassManager
@@ -131,45 +131,45 @@ def installAtEnd (p : Pass) : PassInstaller where
 def append (passesNew : Array Pass) : PassInstaller where
   install passes := return passes ++ passesNew
 
-def withEachOccurence (targetName : Name) (f : Nat → PassInstaller) : PassInstaller where
+def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassInstaller where
   install passes := do
-    let highestOccurence ← PassManager.findHighestOccurence targetName passes
+    let highestOccurrence ← PassManager.findHighestOccurrence targetName passes
     let mut passes := passes
-    for occurence in [0:highestOccurence+1] do
-      passes ← f occurence |>.install passes
+    for occurrence in [0:highestOccurrence+1] do
+      passes ← f occurrence |>.install passes
     return passes
 
-def installAfter (targetName : Name) (p : Pass → Pass) (occurence : Nat := 0) : PassInstaller where
+def installAfter (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where
   install passes :=
-    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurence == occurence) then
+    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
       let passUnderTest := passes[idx]!
       return passes.insertAt (idx + 1) (p passUnderTest)
     else
-      throwError s!"Tried to insert pass after {targetName}, occurence {occurence} but {targetName} is not in the pass list"
+      throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
 def installAfterEach (targetName : Name) (p : Pass → Pass) : PassInstaller :=
-    withEachOccurence targetName (installAfter targetName p ·)
+    withEachOccurrence targetName (installAfter targetName p ·)
 
-def installBefore (targetName : Name) (p : Pass → Pass) (occurence : Nat := 0): PassInstaller where
+def installBefore (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0): PassInstaller where
   install passes :=
-    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurence == occurence) then
+    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
       let passUnderTest := passes[idx]!
       return passes.insertAt idx (p passUnderTest)
     else
-      throwError s!"Tried to insert pass after {targetName}, occurence {occurence} but {targetName} is not in the pass list"
+      throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
-def installBeforeEachOccurence (targetName : Name) (p : Pass → Pass) : PassInstaller :=
-    withEachOccurence targetName (installBefore targetName p ·)
+def installBeforeEachOccurrence (targetName : Name) (p : Pass → Pass) : PassInstaller :=
+    withEachOccurrence targetName (installBefore targetName p ·)
 
-def replacePass (targetName : Name) (p : Pass → Pass) (occurence : Nat := 0) : PassInstaller where
+def replacePass (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where
   install passes := do
-    let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurence == occurence) | throwError s!"Tried to replace {targetName}, occurence {occurence} but {targetName} is not in the pass list"
+    let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) | throwError s!"Tried to replace {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
     let target := passes[idx]!
     let replacement := p target
     return passes.set! idx replacement
 
-def replaceEachOccurence (targetName : Name) (p : Pass → Pass) : PassInstaller :=
-    withEachOccurence targetName (replacePass targetName p ·)
+def replaceEachOccurrence (targetName : Name) (p : Pass → Pass) : PassInstaller :=
+    withEachOccurrence targetName (replacePass targetName p ·)
 
 def run (manager : PassManager) (installer : PassInstaller) : CompilerM PassManager := do
   return { manager with passes := (←installer.install manager.passes) }

stage0/src/Lean/Compiler/LCNF/Passes.lean

@@ -22,8 +22,9 @@ namespace Lean.Compiler.LCNF
     pullFunDecls,
     findJoinPoints,
     reduceJpArity,
-    simp { etaPoly := true, inlinePartial := true, implementedBy := true } (occurence := 1),
-    specialize
+    simp { etaPoly := true, inlinePartial := true, implementedBy := true } (occurrence := 1),
+    specialize,
+    simp (occurrence := 2)
   ]
 
 end Lean.Compiler.LCNF

stage0/src/Lean/Compiler/LCNF/Simp.lean

@@ -855,7 +855,7 @@ simplification opportunities by eta-expanding them.
 def etaPolyApp? (letDecl : LetDecl) : OptionT SimpM FunDecl := do
   guard <| (← read).config.etaPoly
   let .const declName _ := letDecl.value.getAppFn | failure
-  let info ← getConstInfo declName
+  let some info := (← getEnv).find? declName | failure
   guard <| hasLocalInst info.type
   guard <| !(← Meta.isInstance declName)
   let some decl ← getStage1Decl? declName | failure
@@ -959,7 +959,15 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
       They will only be deleted in the next pass.
       -/
       if code.isFun then
-        decl ← decl.etaExpand
+        if decl.isEtaExpandCandidate then
+          /- We must apply substitution before trying to eta-expand, otherwise `inferType` may fail. -/
+          decl ← normFunDecl decl
+          /-
+          We want to eta-expand **before** trying to simplify local function declaration because
+          eta-expansion creates many optimization opportunities.
+          -/
+          decl ← decl.etaExpand
+          markSimplified
       decl ← simpFunDecl decl
     let k ← simp k
     if (← isUsed decl.fvarId) then
@@ -1051,8 +1059,8 @@ where
     else
       return decl
 
-def simp (config : Config := {}) (occurence : Nat := 0) : Pass :=
-  .mkPerDeclaration `simp (Decl.simp · config) .base (occurence := occurence)
+def simp (config : Config := {}) (occurrence : Nat := 0) : Pass :=
+  .mkPerDeclaration `simp (Decl.simp · config) .base (occurrence := occurrence)
 
 builtin_initialize
   registerTraceClass `Compiler.simp (inherited := true)

stage0/src/Lean/Compiler/LCNF/Specialize.lean

@@ -9,10 +9,22 @@ import Lean.Compiler.LCNF.Simp
 import Lean.Compiler.LCNF.SpecInfo
 import Lean.Compiler.LCNF.PrettyPrinter
 import Lean.Compiler.LCNF.ToExpr
+import Lean.Compiler.LCNF.Level
 
 namespace Lean.Compiler.LCNF
 namespace Specialize
 
+abbrev Cache := Std.PHashMap Expr Name
+
+builtin_initialize specCacheExt : EnvExtension Cache ←
+  registerEnvExtension (pure {})
+
+def cacheSpec (key : Expr) (declName : Name) : CoreM Unit :=
+  modifyEnv fun env => specCacheExt.modifyState env (·.insert key declName)
+
+def findSpecCache? (key : Expr) : CoreM (Option Name) :=
+  return specCacheExt.getState (← getEnv) |>.find? key
+
 structure Context where
   /--
   Set of free variables in scope. The "collector" uses this information when collecting
@@ -23,6 +35,10 @@ structure Context where
   Set of let-declarations in scope that do not depend on parameters.
   -/
   ground : FVarIdSet := {}
+  /--
+  Name of the declaration being processed
+  -/
+  declName : Name
 
 structure State where
   decls : Array Decl := #[]
@@ -46,7 +62,7 @@ def isGround (e : Expr) : SpecializeM Bool := do
 @[inline] def withLetDecl (decl : LetDecl) (x : SpecializeM α) : SpecializeM α := do
   let grd ← isGround decl.value
   let fvarId := decl.fvarId
-  withReader (fun { scope, ground } => { scope := scope.insert fvarId, ground := if grd then ground.insert fvarId else ground }) x
+  withReader (fun { scope, ground, declName } => { declName, scope := scope.insert fvarId, ground := if grd then ground.insert fvarId else ground }) x
 
 namespace Collector
 /-!
@@ -204,19 +220,20 @@ end
 /--
 Given the specialization mask `paramsInfo` and the arguments `args`,
 collect their dependencies, and return an array `mask` of size `paramsInfo.size` s.t.
-- `mask[i] = args[i]` if `paramsInfo[i] != .other`
-- `mask[i] = lcErased`, otherwise.
+- `mask[i] = some args[i]` if `paramsInfo[i] != .other`
+- `mask[i] = none`, otherwise.
 That is, `mask` contains only the arguments that are contributing to the code specialization.
-We use this information to compute a "key" to uniquely identify the code specialization.
+We use this information to compute a "key" to uniquely identify the code specialization, and
+creating the specialized code.
 -/
-def collect (paramsInfo : Array SpecParamInfo) (args : Array Expr) : CollectorM (Array Expr) := do
+def collect (paramsInfo : Array SpecParamInfo) (args : Array Expr) : CollectorM (Array (Option Expr)) := do
   let mut argMask := #[]
   for paramInfo in paramsInfo, arg in args do
     match paramInfo with
     | .other =>
-      argMask := argMask.push (mkConst ``lcErased)
+      argMask := argMask.push none
     | .fixedNeutral | .user | .fixedInst | .fixedHO =>
-      argMask := argMask.push arg
+      argMask := argMask.push (some arg)
       collectExpr arg
   return argMask
 
@@ -256,41 +273,102 @@ termination_by go => values.size - i
 /--
 Create the "key" that uniquely identifies a code specialization.
 `params` and `decls` are the declarations collected by the `collect` function above.
+The result contains the list of universe level parameter names the key that `params`, `decls`, and `body` depends on.
+We use this information to create the new auxiliary declaration and resulting application.
 -/
-def mkKey (params : Array Param) (decls : Array CodeDecl) (body : Expr) : CompilerM Expr := do
+def mkKey (params : Array Param) (decls : Array CodeDecl) (body : Expr) : CompilerM (Expr × List Name) := do
   let body ← expandCodeDecls decls body
-  -- TODO: normalize universe level parameters
-  return ToExpr.run do
+  let key := ToExpr.run do
     ToExpr.withParams params do
       ToExpr.mkLambdaM params (← ToExpr.abstractM body)
+  return normLevelParams key
+
+open Internalize in
+/--
+Specialize `decl` using
+- `us`: the universe level used to instantiate `decl.name`
+- `argMask`: arguments that are being used to specialize the declaration.
+- `params`: new parameters that arguments in `argMask` depend on.
+- `decls`: local declarations that arguments in `argMask` depend on.
+- `levelParamsNew`: the universe level parameters for the new declaration.
+-/
+def mkSpecDecl (decl : Decl) (us : List Level) (argMask : Array (Option Expr)) (params : Array Param) (decls : Array CodeDecl) (levelParamsNew : List Name) : SpecializeM Decl := do
+  let nameNew := decl.name ++ `_at_ ++ (← read).declName ++ (`spec).appendIndexAfter (← get).decls.size
+  go nameNew |>.run' {}
+where
+  go (nameNew : Name) : InternalizeM Decl := do
+    let mut params ← params.mapM internalizeParam
+    let decls ← decls.mapM internalizeCodeDecl
+    for param in decl.params, arg in argMask do
+      if let some arg := arg then
+        let arg ← normExpr arg
+        modify fun s => s.insert param.fvarId arg
+      else
+        -- Keep the parameter
+        let param := { param with type := param.type.instantiateLevelParams decl.levelParams us }
+        params := params.push (← internalizeParam param)
+    for param in decl.params[argMask.size:] do
+      let param := { param with type := param.type.instantiateLevelParams decl.levelParams us }
+      params := params.push (← internalizeParam param)
+    let value := decl.instantiateValueLevelParams us
+    let value ← internalizeCode value
+    let value := attachCodeDecls decls value
+    let type ← value.inferType
+    let type ← mkForallParams params type
+    let decl := { name := nameNew, levelParams := levelParamsNew, params, type, value : Decl }
+    return decl.setLevelParams
 
 /--
-Try to specialize the function application in the given let-declaration.
-`k` is the continuation for the let-declaration.
+Given the specialization mask `paramsInfo` and the arguments `args`,
+return the arguments that have not been considered for specialization.
 -/
-def specializeApp? (letDecl : LetDecl) (_k : Code) : SpecializeM (Option Code) := do
-  unless letDecl.value.isApp do return none
-  let f := letDecl.value.getAppFn
-  let .const declName _us := f | return none
-  if (← Meta.isInstance declName) then return none
-  let some paramsInfo ← getSpecParamInfo? declName | return none
-  let args := letDecl.value.getAppArgs
-  unless (← shouldSpecialize paramsInfo args) do return none
-  let some _decl ← getStage1Decl? declName | return none
-  trace[Compiler.specialize.candidate] "{letDecl.value}, {paramsInfo}"
-  let (argMask, { params, decls, .. }) ← Collector.collect paramsInfo args |>.run {}
-  let keyBody := mkAppN f argMask
-  let key ← mkKey params decls keyBody
-  trace[Compiler.specialize.candidate] "key: {key}"
-  assert! !key.hasLooseBVars
-  assert! !key.hasFVar
-  trace[Compiler.specialize.candidate] "decls:  {decls.map fun | .let decl | .jp decl | .fun decl => decl.binderName}"
-  trace[Compiler.specialize.candidate] "params: {params.map fun p => p.binderName}"
-
-  -- TODO
-  return none
+def getRemainingArgs (paramsInfo : Array SpecParamInfo) (args : Array Expr) : Array Expr := Id.run do
+  let mut result := #[]
+  for info in paramsInfo, arg in args do
+    if info matches .other then
+      result := result.push arg
+  return result ++ args[paramsInfo.size:]
 
 mutual
+  /--
+  Try to specialize the function application in the given let-declaration.
+  `k` is the continuation for the let-declaration.
+  -/
+  partial def specializeApp? (e : Expr) : SpecializeM (Option Expr) := do
+    unless e.isApp do return none
+    let f := e.getAppFn
+    let .const declName us := f | return none
+    if (← Meta.isInstance declName) then return none
+    let some paramsInfo ← getSpecParamInfo? declName | return none
+    let args := e.getAppArgs
+    unless (← shouldSpecialize paramsInfo args) do return none
+    let some decl ← getStage1Decl? declName | return none
+    trace[Compiler.specialize.candidate] "{e}, {paramsInfo}"
+    let (argMask, { params, decls, .. }) ← Collector.collect paramsInfo args |>.run {}
+    let keyBody := mkAppN f (argMask.filterMap id)
+    let (key, levelParamsNew) ← mkKey params decls keyBody
+    trace[Compiler.specialize.candidate] "key: {key}"
+    assert! !key.hasLooseBVars
+    assert! !key.hasFVar
+    let usNew := levelParamsNew.map mkLevelParam
+    let argsNew := params.map (mkFVar ·.fvarId) ++ getRemainingArgs paramsInfo args
+    if let some declName ← findSpecCache? key then
+      trace[Compiler.specialize.step] "cached: {declName}"
+      return mkAppN (.const declName usNew) argsNew
+    else
+      let specDecl ← mkSpecDecl decl us argMask params decls levelParamsNew
+      trace[Compiler.specialize.step] "new: {specDecl.name}"
+      cacheSpec key specDecl.name
+      let specDecl ← specDecl.etaExpand
+      saveLCNFType specDecl.name specDecl.type
+      let specDecl ← specDecl.simp {} -- TODO: `simp` config
+      let specDecl ← specDecl.simp { etaPoly := true, inlinePartial := true, implementedBy := true }
+      let value ← withReader (fun _ => { declName := specDecl.name }) do
+         withParams specDecl.params <| visitCode specDecl.value
+      let specDecl := { specDecl with value }
+      modify fun s => { s with decls := s.decls.push specDecl }
+      return mkAppN (.const specDecl.name usNew) argsNew
+
   partial def visitFunDecl (funDecl : FunDecl) : SpecializeM FunDecl := do
     let value ← withParams funDecl.params <| visitCode funDecl.value
     funDecl.update' funDecl.type value
@@ -298,11 +376,11 @@ mutual
   partial def visitCode (code : Code) : SpecializeM Code := do
     match code with
     | .let decl k =>
-      if let some k ← specializeApp? decl k then
-        visitCode k
-      else
-        let k ← withLetDecl decl <| visitCode k
-        return code.updateLet! decl k
+      let mut decl := decl
+      if let some value ← specializeApp? decl.value then
+        decl ← decl.updateValue value
+      let k ← withLetDecl decl <| visitCode k
+      return code.updateLet! decl k
     | .fun decl k | .jp decl k =>
       let decl ← visitFunDecl decl
       let k ← withFVar decl.fvarId <| visitCode k
@@ -327,7 +405,7 @@ def main (decl : Decl) : SpecializeM Decl := do
 end Specialize
 
 partial def Decl.specialize (decl : Decl) : CompilerM (Array Decl) := do
-  let (decl, s) ← Specialize.main decl |>.run {} |>.run {}
+  let (decl, s) ← Specialize.main decl |>.run { declName := decl.name } |>.run {}
   return s.decls.push decl
 
 def specialize : Pass where
@@ -340,5 +418,6 @@ def specialize : Pass where
 builtin_initialize
   registerTraceClass `Compiler.specialize (inherited := true)
   registerTraceClass `Compiler.specialize.candidate
+  registerTraceClass `Compiler.specialize.step
 
 end Lean.Compiler.LCNF

stage0/src/Lean/Compiler/LCNF/Stage1.lean

@@ -37,7 +37,7 @@ def getStage1Decl? (declName : Name) : CoreM (Option Decl) := do
   match stage1Ext.getState (← getEnv) |>.decls.find? declName with
   | some decl => return decl
   | none =>
-    let info ← getConstInfo declName
+    let some info := (← getEnv).find? declName | return none
     if info.hasValue then
       let decls ← compileStage1 info.all.toArray
       return decls.find? fun decl => declName == decl.name

stage0/src/Lean/Compiler/LCNF/Testing.lean

@@ -92,45 +92,45 @@ private def assertAfterTest (test : SimpleTest) : TestInstallerM (Pass → Pass)
     phase := passUnderTest.phase
     name := testName
     run := fun decls => do
-      trace[Compiler.test] s!"Starting post condition test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence}"
+      trace[Compiler.test] s!"Starting post condition test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence}"
       test.run decls passUnderTest testName
-      trace[Compiler.test] s!"Post condition test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence} successful"
+      trace[Compiler.test] s!"Post condition test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence} successful"
       return decls
   }
 
 /--
-Install an assertion pass right after a specific occurence of a pass,
+Install an assertion pass right after a specific occurrence of a pass,
 default is first.
 -/
-def assertAfter (test : SimpleTest) (occurence : Nat := 0): TestInstaller := do
+def assertAfter (test : SimpleTest) (occurrence : Nat := 0): TestInstaller := do
   let passUnderTestName := (←read).passUnderTestName
   let assertion ← assertAfterTest test
-  return .installAfter passUnderTestName assertion occurence
+  return .installAfter passUnderTestName assertion occurrence
 
 /--
-Install an assertion pass right after each occurence of a pass.
+Install an assertion pass right after each occurrence of a pass.
 -/
-def assertAfterEachOccurence (test : SimpleTest) : TestInstaller := do
+def assertAfterEachOccurrence (test : SimpleTest) : TestInstaller := do
   let passUnderTestName := (←read).passUnderTestName
   let assertion ← assertAfterTest test
   return .installAfterEach passUnderTestName assertion
 
 /--
-Install an assertion pass right after a specific occurence of a pass,
+Install an assertion pass right after a specific occurrence of a pass,
 default is first. The assertion operates on a per declaration basis.
 -/
-def assertForEachDeclAfter (assertion : Pass → Decl → Bool) (msg : String) (occurence : Nat := 0) : TestInstaller :=
+def assertForEachDeclAfter (assertion : Pass → Decl → Bool) (msg : String) (occurrence : Nat := 0) : TestInstaller :=
   let assertion := do
     let pass ← getPassUnderTest
     (←getDecls).forM (fun decl => assert (assertion pass decl) msg)
-  assertAfter assertion occurence
+  assertAfter assertion occurrence
 
 /--
-Install an assertion pass right after the each occurence of a pass. The
+Install an assertion pass right after the each occurrence of a pass. The
 assertion operates on a per declaration basis.
 -/
-def assertForEachDeclAfterEachOccurence (assertion : Pass → Decl → Bool) (msg : String) : TestInstaller :=
-  assertAfterEachOccurence <| do
+def assertForEachDeclAfterEachOccurrence (assertion : Pass → Decl → Bool) (msg : String) : TestInstaller :=
+  assertAfterEachOccurrence <| do
     let pass ← getPassUnderTest
     (←getDecls).forM (fun decl => assert (assertion pass decl) msg)
 
@@ -140,32 +140,32 @@ private def assertAroundTest (test : InOutTest) : TestInstallerM (Pass → Pass)
     phase := passUnderTest.phase
     name := passUnderTest.name
     run := fun decls => do
-      trace[Compiler.test] s!"Starting wrapper test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence}"
+      trace[Compiler.test] s!"Starting wrapper test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence}"
       let newDecls ← passUnderTest.run decls
       test.run decls newDecls passUnderTest testName
-      trace[Compiler.test] s!"Wrapper test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence} successful"
+      trace[Compiler.test] s!"Wrapper test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence} successful"
       return newDecls
   }
 
 /--
-Replace a specific occurence, default is first, of a pass with a wrapper one that allows
+Replace a specific occurrence, default is first, of a pass with a wrapper one that allows
 the user to provide an assertion which takes into account both the
 declarations that were sent to and produced by the pass under test.
 -/
-def assertAround (test : InOutTest) (occurence : Nat := 0) : TestInstaller := do
+def assertAround (test : InOutTest) (occurrence : Nat := 0) : TestInstaller := do
   let passUnderTestName := (←read).passUnderTestName
   let assertion ← assertAroundTest test
-  return .replacePass passUnderTestName assertion occurence
+  return .replacePass passUnderTestName assertion occurrence
 
 /--
-Replace all occurences of a pass with a wrapper one that allows
+Replace all occurrences of a pass with a wrapper one that allows
 the user to provide an assertion which takes into account both the
 declarations that were sent to and produced by the pass under test.
 -/
-def assertAroundEachOccurence (test : InOutTest) : TestInstaller := do
+def assertAroundEachOccurrence (test : InOutTest) : TestInstaller := do
   let passUnderTestName := (←read).passUnderTestName
   let assertion ← assertAroundTest test
-  return .replaceEachOccurence passUnderTestName assertion
+  return .replaceEachOccurrence passUnderTestName assertion
 
 private def throwFixPointError (err : String) (firstResult secondResult : Array Decl) : CompilerM Unit := do
   let mut err := err
@@ -195,7 +195,7 @@ def assertIsAtFixPoint : TestInstaller :=
     else if decls != secondResult then
       let err := s!"Pass {passUnderTest.name} did not reach a fixpoint, it either changed declarations or their order:\n"
       throwFixPointError err decls secondResult
-  assertAfterEachOccurence test
+  assertAfterEachOccurrence test
 
 /--
 Compare the overall sizes of the input and output of `passUnderTest` with `assertion`.
@@ -204,7 +204,7 @@ If `assertion inputSize outputSize` is `false` throw an exception with `msg`.
 def assertSize (assertion : Nat → Nat → Bool) (msg : String) : TestInstaller :=
   let sumDeclSizes := fun decls => decls.map Decl.size |>.foldl (init := 0) (· + ·)
   let assertion := (fun inputS outputS => Testing.assert (assertion inputS outputS) s!"{msg}: input size {inputS} output size {outputS}")
-  assertAroundEachOccurence (do assertion (sumDeclSizes (←getInputDecls)) (sumDeclSizes (←getOutputDecls)))
+  assertAroundEachOccurrence (do assertion (sumDeclSizes (←getInputDecls)) (sumDeclSizes (←getOutputDecls)))
 
 /--
 Assert that the overall size of the `Decl`s in the compilation pipeline does not change
@@ -231,7 +231,7 @@ Assert that the pass under test produces `Decl`s that do not contain
 `Expr.const constName` in their `Code.let` values anymore.
 -/
 def assertDoesNotContainConstAfter (constName : Name) (msg : String) : TestInstaller :=
-  assertForEachDeclAfterEachOccurence (fun _ decl => !decl.value.containsConst constName) msg
+  assertForEachDeclAfterEachOccurrence (fun _ decl => !decl.value.containsConst constName) msg
 
 def assertNoFun : TestInstaller :=
   assertAfter do

stage0/src/Lean/Compiler/LCNF/Types.lean

@@ -145,6 +145,13 @@ where
         result := mkApp result erasedExpr
     return result
 
+/--
+Save the LCNF type for the given declaration.
+-/
+def saveLCNFType (declName : Name) (type : Expr) : CoreM Unit := do
+  modifyEnv fun env =>
+    lcnfTypeExt.modifyState env fun s => { s with types := s.types.insert declName type }
+
 /--
 Return the LCNF type for the given declaration.
 -/
@@ -154,7 +161,7 @@ def getDeclLCNFType (declName : Name) : CoreM Expr := do
   | none =>
     let info ← getConstInfo declName
     let type ← Meta.MetaM.run' <| toLCNFType info.type
-    modifyEnv fun env => lcnfTypeExt.modifyState env fun s => { s with types := s.types.insert declName type }
+    saveLCNFType declName type
     return type
 
 /--
@@ -273,8 +280,8 @@ This function is similar to `isTypeFormerType`, but more liberal.
 For example, `isTypeFormerType` returns false for `lcAny` and `Nat → lcAny`, but
 this function returns true.
 -/
-def maybeTypeFormerType (type : Expr) : Bool :=
-  match type with
+partial def maybeTypeFormerType (type : Expr) : Bool :=
+  match type.headBeta with
   | .sort .. => true
   | .forallE _ _ b _ => maybeTypeFormerType b
   | _ => type.isAnyType
@@ -293,13 +300,13 @@ def isClass? (type : Expr) : CoreM (Option Name) := do
 `isArrowClass? type` return `some ClsName` if the LCNF `type` is an instance of the class `ClsName`, or
 if it is arrow producing an instance of the class `ClsName`.
 -/
-def isArrowClass? (type : Expr) : CoreM (Option Name) := do
-  match type with
+partial def isArrowClass? (type : Expr) : CoreM (Option Name) := do
+  match type.headBeta with
   | .forallE _ _ b _ => isArrowClass? b
   | _ => isClass? type
 
-def getArrowArity (e : Expr) :=
-  match e with
+partial def getArrowArity (e : Expr) :=
+  match e.headBeta with
   | .forallE _ _ b _ => getArrowArity b + 1
   | _ => 0
 

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

@@ -35,42 +35,75 @@ open Parser.Tactic
 @[builtinTactic paren] def evalParen : Tactic := fun stx =>
   evalTactic stx[1]
 
-def isCheckpointableTactic (arg : Syntax.Tactic) : TacticM Bool := do
+def isCheckpointableTactic (arg : Syntax) : TacticM Bool := do
   -- TODO: make it parametric
-  let kind := arg.1.getKind
+  let kind := arg.getKind
   return kind == ``Lean.Parser.Tactic.save
 
-partial def addCheckpoints (args : Array Syntax.Tactic) : TacticM (Array Syntax.Tactic) := do
-  -- if (← readThe Term.Context).tacticCache? |>.isSome then
-  if (← args.anyM fun arg => isCheckpointableTactic arg) then
-    let argsNew ← go 0 #[] #[]
-    return argsNew
-  return args
-where
-  push (acc : Array Syntax.Tactic) (result : Array Syntax.Tactic) : Array Syntax.Tactic :=
-    if acc.isEmpty then
-      result
-    else
-      result.push <| Unhygienic.run do withRef acc.back do
-        `(tactic| checkpoint $[$acc]*)
+/--
+Takes a `sepByIndent tactic "; "`, and inserts `checkpoint` blocks for `save` tactics.
 
-  go (i : Nat) (acc : Array Syntax.Tactic) (result : Array Syntax.Tactic) : TacticM (Array Syntax.Tactic) := do
-    if h : i < args.size then
-      let arg := args.get ⟨i, h⟩
-      if (← isCheckpointableTactic arg) then
-        -- `argNew` is `arg` as singleton sequence. The idea is to make sure it does not satisfy `isCheckpointableTactic` anymore
-        let argNew := ⟨mkNullNode #[arg]⟩ -- HACK
-        let acc := acc.push argNew
-        go (i+1) #[] (push acc result)
-      else
-        go (i+1) (acc.push arg) result
+Input:
+```
+  a
+  b
+  save
+  c
+  d
+  save
+  e
+```
+
+Output:
+```
+  checkpoint
+    a
+    b
+    save
+  checkpoint
+    c
+    d
+    save
+  e
+```
+-/
+-- Note that we need to preserve the separators to show the right goals after semicolons.
+def addCheckpoints (stx : Syntax) : TacticM Syntax := do
+  -- if (← readThe Term.Context).tacticCache? |>.isSome then
+  if !(← stx.getSepArgs.anyM isCheckpointableTactic) then return stx
+  let mut currentCheckpointBlock := #[]
+  let mut output := #[]
+  for i in [:stx.getArgs.size / 2] do
+    let tac := stx[2*i]
+    let sep? := stx.getArgs[2*i+1]?
+    if (← isCheckpointableTactic tac) then
+      let checkpoint : Syntax :=
+        mkNode ``checkpoint #[
+          mkAtomFrom tac "checkpoint",
+          mkNode ``tacticSeq #[
+            mkNode ``tacticSeq1Indented #[
+              -- HACK: null node is not a valid tactic, but prevents infinite loop
+              mkNullNode (currentCheckpointBlock.push tac)
+            ]
+          ]
+        ]
+      currentCheckpointBlock := #[]
+      output := output.push checkpoint
+      if let some sep := sep? then output := output.push sep
     else
-      return result ++ acc
+      currentCheckpointBlock := currentCheckpointBlock.push tac
+      if let some sep := sep? then currentCheckpointBlock := currentCheckpointBlock.push sep
+  output := output ++ currentCheckpointBlock
+  return stx.setArgs output
 
 /-- Evaluate `sepByIndent tactic "; " -/
 def evalSepByIndentTactic (stx : Syntax) : TacticM Unit := do
-  for seqElem in (← addCheckpoints (stx.getSepArgs.map (⟨·⟩))) do
-    evalTactic seqElem
+  let stx ← addCheckpoints stx
+  for arg in stx.getArgs, i in [:stx.getArgs.size] do
+    if i % 2 == 0 then
+      evalTactic arg
+    else
+      saveTacticInfoForToken arg
 
 @[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx =>
   evalSepByIndentTactic stx[0]

stage0/src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -85,17 +85,23 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
    withMainContext do
      changeLhs (← zetaReduce (← getLhs))
 
+/-- Evaluate `sepByIndent conv "; " -/
+def evalSepByIndentConv (stx : Syntax) : TacticM Unit := do
+  for arg in stx.getArgs, i in [:stx.getArgs.size] do
+    if i % 2 == 0 then
+      evalTactic arg
+    else
+      saveTacticInfoForToken arg
+
 @[builtinTactic Lean.Parser.Tactic.Conv.convSeq1Indented] def evalConvSeq1Indented : Tactic := fun stx => do
-  for seqElem in stx[0].getSepArgs do
-    evalTactic seqElem
+  evalSepByIndentConv stx[0]
 
 @[builtinTactic Lean.Parser.Tactic.Conv.convSeqBracketed] def evalConvSeqBracketed : Tactic := fun stx => do
   let initInfo ← mkInitialTacticInfo stx[0]
   withRef stx[2] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `{`
     withInfoContext (pure ()) initInfo
-    for seqElem in stx[1].getSepArgs do
-      evalTactic seqElem
+    evalSepByIndentConv stx[1]
     evalTactic (← `(tactic| all_goals (try rfl)))
 
 @[builtinTactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do

stage0/src/Lean/MetavarContext.lean

@@ -240,9 +240,14 @@ def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : Local
   | some idx => localInsts.eraseIdx idx
   | _        => localInsts
 
+/-- A kind for the metavariable that determines its unification behaviour.
+For more information see the large comment at the beginning of this file. -/
 inductive MetavarKind where
+  /-- Normal unification behaviour -/
   | natural
+  /-- `isDefEq` avoids assignment -/
   | synthetic
+  /-- Never assigned by isDefEq -/
   | syntheticOpaque
   deriving Inhabited, Repr
 
@@ -254,9 +259,13 @@ def MetavarKind.isNatural : MetavarKind → Bool
   | MetavarKind.natural => true
   | _                   => false
 
+/-- Information about a metavariable. -/
 structure MetavarDecl where
+  /-- A user-friendly name for the metavariable. If anonymous then there is no such name. -/
   userName       : Name := Name.anonymous
+  /-- The local context containing the free variables that the mvar is permitted to depend upon. -/
   lctx           : LocalContext
+  /-- The type of the metavarible, in the given `lctx`. -/
   type           : Expr
   /--
     The nesting depth of this metavariable. We do not want
@@ -268,8 +277,10 @@ structure MetavarDecl where
   depth          : Nat
   localInstances : LocalInstances
   kind           : MetavarKind
-  numScopeArgs   : Nat := 0 -- See comment at `CheckAssignment` `Meta/ExprDefEq.lean`
-  index          : Nat      -- We use this field to track how old a metavariable is. It is set using a counter at `MetavarContext`
+  /-- See comment at `CheckAssignment` `Meta/ExprDefEq.lean` -/
+  numScopeArgs   : Nat := 0
+  /-- We use this field to track how old a metavariable is. It is set using a counter at `MetavarContext` -/
+  index          : Nat
   deriving Inhabited
 
 /--
@@ -292,16 +303,29 @@ structure DelayedMetavarAssignment where
 
 open Std (HashMap PersistentHashMap)
 
+/-- The metavariable context is a set of metavariable declarations and their assignments.
+
+For more information on specifics see the comment in the file that `MetavarContext` is defined in.
+-/
 structure MetavarContext where
+  /-- Depth is used to control whether an mvar can be assigned in unification. -/
   depth          : Nat := 0
-  mvarCounter    : Nat := 0 -- Counter for setting the field `index` at `MetavarDecl`
+  /-- Counter for setting the field `index` at `MetavarDecl` -/
+  mvarCounter    : Nat := 0
   lDepth         : PersistentHashMap LMVarId Nat := {}
+  /-- Metavariable declarations. -/
   decls          : PersistentHashMap MVarId MetavarDecl := {}
+  /-- Index mapping user-friendly names to ids. -/
   userNames      : PersistentHashMap Name MVarId := {}
+  /-- Assignment table for universe level metavariables.-/
   lAssignment    : PersistentHashMap LMVarId Level := {}
+  /-- Assignment table for expression metavariables.-/
   eAssignment    : PersistentHashMap MVarId Expr := {}
+  /-- Assignment table for delayed abstraction metavariables.
+  For more information about delayed abstraction, see the docstring for `DelayedMetavarAssignment`. -/
   dAssignment    : PersistentHashMap MVarId DelayedMetavarAssignment := {}
 
+/-- A monad with a stateful metavariable context, defining `getMCtx` and `modifyMCtx`. -/
 class MonadMCtx (m : Type → Type) where
   getMCtx    : m MetavarContext
   modifyMCtx : (MetavarContext → MetavarContext) → m Unit
@@ -451,7 +475,7 @@ def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
 def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvarIdPending : MVarId) : m Unit :=
   modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending } }
 
-/--
+/-!
 Notes on artificial eta-expanded terms due to metavariables.
 We try avoid synthetic terms such as `((fun x y => t) a b)` in the output produced by the elaborator.
 This kind of term may be generated when instantiating metavariable assignments.
@@ -469,6 +493,7 @@ We address this issue by create a synthetic metavariable `?n : Nat → Nat` and
 To avoid this term eta-expanded term, we apply beta-reduction when instantiating metavariable assignments in this module.
 This operation is performed at `instantiateExprMVars`, `elimMVarDeps`, and `levelMVarToParam`.
 -/
+
 partial def instantiateLevelMVars [Monad m] [MonadMCtx m] : Level → m Level
   | lvl@(Level.succ lvl₁)      => return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁)
   | lvl@(Level.max lvl₁ lvl₂)  => return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂)

stage0/src/Lean/Parser/Extra.lean

@@ -72,7 +72,9 @@ def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : F
   let hasNewlineSep := stx.getArgs.mapIdx (fun ⟨i, _⟩ n => i % 2 == 1 && n.matchesNull 0) |>.any id
   visitArgs do
     for i in (List.range stx.getArgs.size).reverse do
-      if i % 2 == 0 then p else pSep <|> (pushWhitespace "\n" *> goLeft)
+      if i % 2 == 0 then p else pSep <|>
+        -- If the final separator is a newline, skip it.
+        ((if i == stx.getArgs.size - 1 then pure () else pushWhitespace "\n") *> goLeft)
   -- If there is any newline separator, then we need to force a newline at the
   -- start so that `withPosition` will pick up the right column.
   if hasNewlineSep then

stage0/src/Lean/Util/CollectLevelParams.lean

@@ -24,11 +24,11 @@ mutual
     else collect u { s with visitedLevel := s.visitedLevel.insert u }
 
   partial def collect : Level → Visitor
-    | Level.succ v    => visitLevel v
-    | Level.max u v   => visitLevel v ∘ visitLevel u
-    | Level.imax u v  => visitLevel v ∘ visitLevel u
-    | Level.param n   => fun s => { s with params := s.params.push n }
-    | _                 => id
+    | .succ v    => visitLevel v
+    | .max u v   => visitLevel v ∘ visitLevel u
+    | .imax u v  => visitLevel v ∘ visitLevel u
+    | .param n   => fun s => { s with params := s.params.push n }
+    | _          => id
 end
 
 mutual
@@ -38,15 +38,15 @@ mutual
     else main e { s with visitedExpr := s.visitedExpr.insert e }
 
   partial def main : Expr → Visitor
-    | Expr.proj _ _ s      => visitExpr s
-    | Expr.forallE _ d b _ => visitExpr b ∘ visitExpr d
-    | Expr.lam _ d b _     => visitExpr b ∘ visitExpr d
-    | Expr.letE _ t v b _  => visitExpr b ∘ visitExpr v ∘ visitExpr t
-    | Expr.app f a         => visitExpr a ∘ visitExpr f
-    | Expr.mdata _ b       => visitExpr b
-    | Expr.const _ us      => fun s => us.foldl (fun s u => visitLevel u s) s
-    | Expr.sort u          => visitLevel u
-    | _                    => id
+    | .proj _ _ s      => visitExpr s
+    | .forallE _ d b _ => visitExpr b ∘ visitExpr d
+    | .lam _ d b _     => visitExpr b ∘ visitExpr d
+    | .letE _ t v b _  => visitExpr b ∘ visitExpr v ∘ visitExpr t
+    | .app f a         => visitExpr a ∘ visitExpr f
+    | .mdata _ b       => visitExpr b
+    | .const _ us      => fun s => us.foldl (fun s u => visitLevel u s) s
+    | .sort u          => visitLevel u
+    | _                => id
 end
 
 partial def State.getUnusedLevelParam (s : CollectLevelParams.State) (pre : Name := `v) : Level :=

stage0/stdlib/Lean/Compiler/LCNF/Bind.c

@@ -21,16 +21,18 @@ lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Code_bind_go___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_uget(lean_object*, size_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkNewParams_go(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__1;
 lean_object* l_Array_append___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Code_bind_go___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT uint8_t l_Lean_Compiler_LCNF_FunDeclCore_isEtaExpandCandidate(lean_object*);
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__2___closed__6;
+static lean_object* l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__1;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__2;
+static lean_object* l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__2;
 lean_object* l_Lean_Compiler_LCNF_mkCasesResultType(lean_object*, 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_EXPORT lean_object* l_Lean_Compiler_LCNF_isEtaExpandCandidateCore___boxed(lean_object*, lean_object*);
 uint8_t lean_usize_dec_lt(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkNewParams___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
@@ -41,6 +43,7 @@ lean_object* l_Lean_Compiler_LCNF_instantiateForall_go(lean_object*, lean_object
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__2___closed__3;
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__2___closed__5;
 lean_object* l_Lean_Compiler_LCNF_getArrowArity(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_FunDeclCore_isEtaExpandCandidate___boxed(lean_object*);
 uint8_t l_Lean_Name_quickCmp(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
@@ -53,15 +56,16 @@ uint8_t l_Array_isEmpty___rarg(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Code_bind_go___closed__1;
 lean_object* l_Std_RBNode_insert___at___private_Lean_Compiler_LCNF_Basic_0__Lean_Compiler_LCNF_collectExpr___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_updateFunDeclImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Code_bind_go___closed__4;
 size_t lean_usize_of_nat(lean_object*);
+LEAN_EXPORT uint8_t l_Lean_Compiler_LCNF_isEtaExpandCandidateCore(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_bind(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_mkAuxLetDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_bind_go___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_fvar___override(lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_RBNode_findCore___at_Lean_Compiler_LCNF_Code_bind_go___spec__1(lean_object*, lean_object*);
-uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_bind_go___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext(lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__2___closed__2;
@@ -71,12 +75,13 @@ lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkNewParams(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_bind_go(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_bind_go___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_InferType_mkForallParams___spec__1(size_t, size_t, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_mkAuxParam(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkNewParams_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_mkNewParams_go___closed__1;
 static lean_object* l_Lean_Compiler_LCNF_Code_bind_go___closed__3;
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_RBNode_findCore___at_Lean_Compiler_LCNF_Code_bind_go___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -1612,7 +1617,52 @@ lean_dec(x_2);
 return x_6;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__1() {
+LEAN_EXPORT uint8_t l_Lean_Compiler_LCNF_isEtaExpandCandidateCore(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_3 = l_Lean_Compiler_LCNF_getArrowArity(x_1);
+x_4 = lean_array_get_size(x_2);
+x_5 = lean_nat_dec_lt(x_4, x_3);
+lean_dec(x_3);
+lean_dec(x_4);
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_isEtaExpandCandidateCore___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = l_Lean_Compiler_LCNF_isEtaExpandCandidateCore(x_1, x_2);
+lean_dec(x_2);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+LEAN_EXPORT uint8_t l_Lean_Compiler_LCNF_FunDeclCore_isEtaExpandCandidate(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; uint8_t x_4; 
+x_2 = lean_ctor_get(x_1, 3);
+lean_inc(x_2);
+x_3 = lean_ctor_get(x_1, 2);
+lean_inc(x_3);
+lean_dec(x_1);
+x_4 = l_Lean_Compiler_LCNF_isEtaExpandCandidateCore(x_2, x_3);
+lean_dec(x_3);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_FunDeclCore_isEtaExpandCandidate___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_Compiler_LCNF_FunDeclCore_isEtaExpandCandidate(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -1620,23 +1670,23 @@ x_1 = lean_mk_string_from_bytes("_x", 2);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__2() {
+static lean_object* _init_l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__1;
+x_2 = l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__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) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore___lambda__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:
 {
 lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
 x_7 = l_Lean_Expr_fvar___override(x_2);
 x_8 = l_Lean_mkAppN(x_7, x_1);
-x_9 = l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__2;
+x_9 = l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__2;
 x_10 = l_Lean_Compiler_LCNF_mkAuxLetDecl(x_8, x_9, x_3, x_4, x_5, x_6);
 if (lean_obj_tag(x_10) == 0)
 {
@@ -1701,147 +1751,198 @@ return x_25;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore_x3f(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_object* x_7) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore(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_object* x_7) {
 _start:
 {
-lean_object* x_8; lean_object* x_9; uint8_t x_10; 
-x_8 = l_Lean_Compiler_LCNF_getArrowArity(x_1);
-x_9 = lean_array_get_size(x_2);
-x_10 = lean_nat_dec_le(x_8, x_9);
-lean_dec(x_9);
-lean_dec(x_8);
-if (x_10 == 0)
-{
-lean_object* x_11; lean_object* x_12; 
-x_11 = lean_unsigned_to_nat(0u);
+lean_object* x_8; lean_object* x_9; 
+x_8 = lean_unsigned_to_nat(0u);
 lean_inc(x_5);
 lean_inc(x_2);
-x_12 = l_Lean_Compiler_LCNF_instantiateForall_go(x_2, x_1, x_11, x_5, x_6, x_7);
-if (lean_obj_tag(x_12) == 0)
+x_9 = l_Lean_Compiler_LCNF_instantiateForall_go(x_2, x_1, x_8, x_5, x_6, x_7);
+if (lean_obj_tag(x_9) == 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; size_t x_20; size_t x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; size_t x_17; size_t x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
+x_10 = lean_ctor_get(x_9, 0);
+lean_inc(x_10);
+x_11 = lean_ctor_get(x_9, 1);
+lean_inc(x_11);
+lean_dec(x_9);
+x_12 = l_Lean_Compiler_LCNF_mkNewParams(x_10, x_4, x_5, x_6, x_11);
 x_13 = lean_ctor_get(x_12, 0);
 lean_inc(x_13);
 x_14 = lean_ctor_get(x_12, 1);
 lean_inc(x_14);
 lean_dec(x_12);
-x_15 = l_Lean_Compiler_LCNF_mkNewParams(x_13, x_4, x_5, x_6, x_14);
-x_16 = lean_ctor_get(x_15, 0);
-lean_inc(x_16);
-x_17 = lean_ctor_get(x_15, 1);
-lean_inc(x_17);
-lean_dec(x_15);
-lean_inc(x_16);
-x_18 = l_Array_append___rarg(x_2, x_16);
-x_19 = lean_array_get_size(x_16);
-x_20 = lean_usize_of_nat(x_19);
-lean_dec(x_19);
-x_21 = 0;
-x_22 = l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_InferType_mkForallParams___spec__1(x_20, x_21, x_16);
-x_23 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1), 6, 1);
-lean_closure_set(x_23, 0, x_22);
-x_24 = l_Lean_Compiler_LCNF_Code_bind(x_3, x_23, x_4, x_5, x_6, x_17);
-if (lean_obj_tag(x_24) == 0)
+lean_inc(x_13);
+x_15 = l_Array_append___rarg(x_2, x_13);
+x_16 = lean_array_get_size(x_13);
+x_17 = lean_usize_of_nat(x_16);
+lean_dec(x_16);
+x_18 = 0;
+x_19 = l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_InferType_mkForallParams___spec__1(x_17, x_18, x_13);
+x_20 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_etaExpandCore___lambda__1), 6, 1);
+lean_closure_set(x_20, 0, x_19);
+x_21 = l_Lean_Compiler_LCNF_Code_bind(x_3, x_20, x_4, x_5, x_6, x_14);
+if (lean_obj_tag(x_21) == 0)
 {
-uint8_t x_25; 
-x_25 = !lean_is_exclusive(x_24);
-if (x_25 == 0)
+uint8_t x_22; 
+x_22 = !lean_is_exclusive(x_21);
+if (x_22 == 0)
 {
-lean_object* x_26; lean_object* x_27; lean_object* x_28; 
-x_26 = lean_ctor_get(x_24, 0);
+lean_object* x_23; lean_object* x_24; 
+x_23 = lean_ctor_get(x_21, 0);
+x_24 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_24, 0, x_15);
+lean_ctor_set(x_24, 1, x_23);
+lean_ctor_set(x_21, 0, x_24);
+return x_21;
+}
+else
+{
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_25 = lean_ctor_get(x_21, 0);
+x_26 = lean_ctor_get(x_21, 1);
+lean_inc(x_26);
+lean_inc(x_25);
+lean_dec(x_21);
 x_27 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_27, 0, x_18);
-lean_ctor_set(x_27, 1, x_26);
-x_28 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_27, 0, x_15);
+lean_ctor_set(x_27, 1, x_25);
+x_28 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_28, 0, x_27);
-lean_ctor_set(x_24, 0, x_28);
-return x_24;
+lean_ctor_set(x_28, 1, x_26);
+return x_28;
+}
 }
 else
 {
-lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_29 = lean_ctor_get(x_24, 0);
-x_30 = lean_ctor_get(x_24, 1);
+uint8_t x_29; 
+lean_dec(x_15);
+x_29 = !lean_is_exclusive(x_21);
+if (x_29 == 0)
+{
+return x_21;
+}
+else
+{
+lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+x_30 = lean_ctor_get(x_21, 0);
+x_31 = lean_ctor_get(x_21, 1);
+lean_inc(x_31);
 lean_inc(x_30);
-lean_inc(x_29);
-lean_dec(x_24);
-x_31 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_31, 0, x_18);
-lean_ctor_set(x_31, 1, x_29);
-x_32 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_32, 0, x_31);
-x_33 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_33, 0, x_32);
-lean_ctor_set(x_33, 1, x_30);
-return x_33;
-}
-}
-else
-{
-uint8_t x_34; 
-lean_dec(x_18);
-x_34 = !lean_is_exclusive(x_24);
-if (x_34 == 0)
-{
-return x_24;
-}
-else
-{
-lean_object* x_35; lean_object* x_36; lean_object* x_37; 
-x_35 = lean_ctor_get(x_24, 0);
-x_36 = lean_ctor_get(x_24, 1);
-lean_inc(x_36);
-lean_inc(x_35);
-lean_dec(x_24);
-x_37 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_37, 0, x_35);
-lean_ctor_set(x_37, 1, x_36);
-return x_37;
+lean_dec(x_21);
+x_32 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_32, 0, x_30);
+lean_ctor_set(x_32, 1, x_31);
+return x_32;
 }
 }
 }
 else
 {
-uint8_t x_38; 
+uint8_t x_33; 
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-x_38 = !lean_is_exclusive(x_12);
-if (x_38 == 0)
+x_33 = !lean_is_exclusive(x_9);
+if (x_33 == 0)
 {
-return x_12;
+return x_9;
 }
 else
 {
-lean_object* x_39; lean_object* x_40; lean_object* x_41; 
-x_39 = lean_ctor_get(x_12, 0);
-x_40 = lean_ctor_get(x_12, 1);
-lean_inc(x_40);
-lean_inc(x_39);
-lean_dec(x_12);
-x_41 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_41, 0, x_39);
-lean_ctor_set(x_41, 1, x_40);
-return x_41;
+lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+x_34 = lean_ctor_get(x_9, 0);
+x_35 = lean_ctor_get(x_9, 1);
+lean_inc(x_35);
+lean_inc(x_34);
+lean_dec(x_9);
+x_36 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_36, 0, x_34);
+lean_ctor_set(x_36, 1, x_35);
+return x_36;
 }
 }
 }
-else
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_etaExpandCore_x3f(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_object* x_7) {
+_start:
 {
-lean_object* x_42; lean_object* x_43; 
+uint8_t x_8; 
+lean_inc(x_1);
+x_8 = l_Lean_Compiler_LCNF_isEtaExpandCandidateCore(x_1, x_2);
+if (x_8 == 0)
+{
+lean_object* x_9; lean_object* x_10; 
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_42 = lean_box(0);
-x_43 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_43, 0, x_42);
-lean_ctor_set(x_43, 1, x_7);
-return x_43;
+x_9 = lean_box(0);
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_7);
+return x_10;
+}
+else
+{
+lean_object* x_11; 
+x_11 = l_Lean_Compiler_LCNF_etaExpandCore(x_1, x_2, x_3, x_4, x_5, x_6, 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; 
+x_13 = lean_ctor_get(x_11, 0);
+x_14 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_14, 0, x_13);
+lean_ctor_set(x_11, 0, x_14);
+return x_11;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_15 = lean_ctor_get(x_11, 0);
+x_16 = lean_ctor_get(x_11, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_11);
+x_17 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_17, 0, x_15);
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_17);
+lean_ctor_set(x_18, 1, x_16);
+return x_18;
+}
+}
+else
+{
+uint8_t x_19; 
+x_19 = !lean_is_exclusive(x_11);
+if (x_19 == 0)
+{
+return x_11;
+}
+else
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_20 = lean_ctor_get(x_11, 0);
+x_21 = lean_ctor_get(x_11, 1);
+lean_inc(x_21);
+lean_inc(x_20);
+lean_dec(x_11);
+x_22 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_22, 0, x_20);
+lean_ctor_set(x_22, 1, x_21);
+return x_22;
+}
+}
 }
 }
 }
@@ -2148,10 +2249,10 @@ l_Lean_Compiler_LCNF_Code_bind_go___closed__4 = _init_l_Lean_Compiler_LCNF_Code_
 lean_mark_persistent(l_Lean_Compiler_LCNF_Code_bind_go___closed__4);
 l_Lean_Compiler_LCNF_mkNewParams_go___closed__1 = _init_l_Lean_Compiler_LCNF_mkNewParams_go___closed__1();
 lean_mark_persistent(l_Lean_Compiler_LCNF_mkNewParams_go___closed__1);
-l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__1 = _init_l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__1();
-lean_mark_persistent(l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__1);
-l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__2 = _init_l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__2();
-lean_mark_persistent(l_Lean_Compiler_LCNF_etaExpandCore_x3f___lambda__1___closed__2);
+l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__1 = _init_l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__1();
+lean_mark_persistent(l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__1);
+l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__2 = _init_l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__2();
+lean_mark_persistent(l_Lean_Compiler_LCNF_etaExpandCore___lambda__1___closed__2);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Compiler/LCNF/Check.c

@@ -913,6 +913,7 @@ x_17 = lean_alloc_closure((void*)(l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF
 lean_closure_set(x_17, 0, x_1);
 lean_closure_set(x_17, 1, x_2);
 lean_closure_set(x_17, 2, x_3);
+lean_inc(x_4);
 x_18 = l_Lean_Compiler_LCNF_maybeTypeFormerType(x_4);
 if (x_18 == 0)
 {

stage0/stdlib/Lean/Compiler/LCNF/InferType.c

@@ -10836,37 +10836,40 @@ return x_9;
 }
 else
 {
-if (lean_obj_tag(x_2) == 7)
+lean_object* x_10; lean_object* x_11; 
+x_10 = lean_array_fget(x_1, x_3);
+x_11 = l_Lean_Expr_headBeta(x_2);
+if (lean_obj_tag(x_11) == 7)
 {
-lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_10 = lean_ctor_get(x_2, 2);
-lean_inc(x_10);
-lean_dec(x_2);
-x_11 = lean_array_fget(x_1, x_3);
-x_12 = lean_ctor_get(x_11, 0);
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_12 = lean_ctor_get(x_11, 2);
 lean_inc(x_12);
 lean_dec(x_11);
-x_13 = l_Lean_Expr_fvar___override(x_12);
-x_14 = lean_expr_instantiate1(x_10, x_13);
-lean_dec(x_13);
+x_13 = lean_ctor_get(x_10, 0);
+lean_inc(x_13);
 lean_dec(x_10);
-x_15 = lean_unsigned_to_nat(1u);
-x_16 = lean_nat_add(x_3, x_15);
+x_14 = l_Lean_Expr_fvar___override(x_13);
+x_15 = lean_expr_instantiate1(x_12, x_14);
+lean_dec(x_14);
+lean_dec(x_12);
+x_16 = lean_unsigned_to_nat(1u);
+x_17 = lean_nat_add(x_3, x_16);
 lean_dec(x_3);
-x_2 = x_14;
-x_3 = x_16;
+x_2 = x_15;
+x_3 = x_17;
 goto _start;
 }
 else
 {
-lean_object* x_18; lean_object* x_19; 
+lean_object* x_19; lean_object* x_20; 
+lean_dec(x_11);
+lean_dec(x_10);
 lean_dec(x_3);
-lean_dec(x_2);
 lean_dec(x_1);
-x_18 = l_Lean_Compiler_LCNF_instantiateForall_go___closed__2;
-x_19 = l_Lean_throwError___at_Lean_Compiler_LCNF_instantiateForall_go___spec__1(x_18, x_4, x_5, x_6);
+x_19 = l_Lean_Compiler_LCNF_instantiateForall_go___closed__2;
+x_20 = l_Lean_throwError___at_Lean_Compiler_LCNF_instantiateForall_go___spec__1(x_19, x_4, x_5, x_6);
 lean_dec(x_4);
-return x_19;
+return x_20;
 }
 }
 }

stage0/stdlib/Lean/Compiler/LCNF/PassManager.c

@@ -17,6 +17,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Pass_mkP
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____lambda__2___closed__2;
 lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addMessageContextPartial___at_Lean_Core_instAddMessageContextCoreM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_replacePass(lean_object*, lean_object*, lean_object*);
 size_t lean_usize_add(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_instInhabitedPass;
@@ -31,6 +32,7 @@ static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compil
 lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__8;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____lambda__3___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_instToStringPhase(uint8_t);
 lean_object* l_Lean_throwError___at_Lean_registerTagAttribute___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -43,6 +45,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_append(lean_object*)
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_append___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_ofExcept___at___private_Lean_Compiler_LCNF_PassManager_0__Lean_Compiler_LCNF_PassInstaller_getPassInstallerUnsafe___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installBefore___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installBefore___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2(lean_object*, size_t, size_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -72,8 +75,7 @@ lean_object* lean_string_append(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____closed__11;
 lean_object* l_Lean_getConstInfo___at___private_Lean_Compiler_InlineAttrs_0__Lean_Compiler_isValidMacroInline___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Compiler_LCNF_PassManager_0__Lean_Compiler_LCNF_PassInstaller_getPassInstallerUnsafe___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Pass_occurence___default;
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1163____spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Phase_instToStringPhase___closed__1;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__8;
@@ -81,7 +83,6 @@ static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__2;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_toNat___boxed(lean_object*);
 uint8_t lean_usize_dec_lt(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Pass_mkPerDeclaration___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurence(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__1;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____closed__8;
@@ -101,6 +102,7 @@ static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compil
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_instInhabitedPassManager;
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_validate___spec__1___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_noConfusion___rarg___lambda__1___boxed(lean_object*);
+static lean_object* l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___closed__1;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__9;
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_validate___spec__1___closed__1;
 lean_object* lean_array_fget(lean_object*, lean_object*);
@@ -133,11 +135,12 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_replacePass___elambd
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1163____lambda__1___boxed(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAtEnd___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassManager_findHighestOccurence(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence(lean_object*, lean_object*);
 lean_object* l_Nat_repr(lean_object*);
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1163____closed__6;
 lean_object* lean_st_mk_ref(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_instHashableExpr;
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassInstaller_addPass___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
@@ -154,27 +157,25 @@ static lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___closed__5;
 lean_object* l_Lean_registerBuiltinAttribute(lean_object*, lean_object*);
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_throwError___at_Lean_AttributeImpl_erase___default___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Compiler_LCNF_instInhabitedPhase;
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_PassManager_0__Lean_Compiler_LCNF_PassInstaller_getPassInstallerUnsafe___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___closed__3;
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installBeforeEachOccurence(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__12;
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAtEnd(lean_object*);
 lean_object* l_Lean_ConstantInfo_type(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurrence(lean_object*, lean_object*);
 lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_append___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Environment_evalConstCheck___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___closed__9;
-LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____closed__19;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_instDecidableLePhaseInstLEPhase___boxed(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___closed__8;
 lean_object* lean_list_to_array(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Pass_occurrence___default;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____closed__5;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___closed__4;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@@ -182,9 +183,9 @@ static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compil
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_noConfusion___rarg___lambda__1(lean_object*);
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__10;
-LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_addPass___closed__2;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_toCtorIdx___boxed(lean_object*);
@@ -231,7 +232,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Pass_mkPerDeclaration___boxed(lean
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____closed__21;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1163____lambda__1(lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_PassManager_findHighestOccurence___closed__1;
+LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_noConfusion(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____closed__6;
 lean_object* l_Array_insertAt___rarg(lean_object*, lean_object*, lean_object*);
@@ -239,10 +240,9 @@ static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compil
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_noConfusion___rarg(uint8_t, uint8_t, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2___closed__3;
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__15;
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_instLEPhase;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_instLTPhase;
-LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installBeforeEachOccurrence(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_instInhabitedPass___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl___closed__14;
@@ -342,7 +342,7 @@ x_1 = 0;
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_Pass_occurence___default() {
+static lean_object* _init_l_Lean_Compiler_LCNF_Pass_occurrence___default() {
 _start:
 {
 lean_object* x_1; 
@@ -1224,7 +1224,7 @@ lean_dec(x_1);
 return x_6;
 }
 }
-LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__1(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__1(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
 _start:
 {
 uint8_t x_10; 
@@ -1272,7 +1272,7 @@ goto _start;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__2(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_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; 
@@ -1349,15 +1349,15 @@ return x_30;
 }
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_PassManager_findHighestOccurence___closed__1() {
+static lean_object* _init_l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("Could not find any occurence of ", 32);
+x_1 = lean_mk_string_from_bytes("Could not find any occurrence of ", 33);
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassManager_findHighestOccurence(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_Lean_Compiler_LCNF_PassManager_findHighestOccurrence(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; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11; lean_object* x_12; 
@@ -1366,7 +1366,7 @@ x_8 = lean_array_get_size(x_2);
 x_9 = lean_usize_of_nat(x_8);
 lean_dec(x_8);
 x_10 = 0;
-x_11 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__1(x_1, x_2, x_9, x_10, x_7, x_3, x_4, x_5, x_6);
+x_11 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__1(x_1, x_2, x_9, x_10, x_7, x_3, x_4, x_5, x_6);
 lean_dec(x_2);
 x_12 = lean_ctor_get(x_11, 0);
 lean_inc(x_12);
@@ -1378,7 +1378,7 @@ lean_inc(x_13);
 lean_dec(x_11);
 x_14 = 1;
 x_15 = l_Lean_Name_toString(x_1, x_14);
-x_16 = l_Lean_Compiler_LCNF_PassManager_findHighestOccurence___closed__1;
+x_16 = l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___closed__1;
 x_17 = lean_string_append(x_16, x_15);
 lean_dec(x_15);
 x_18 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2___closed__1;
@@ -1387,7 +1387,7 @@ x_20 = lean_alloc_ctor(2, 1, 0);
 lean_ctor_set(x_20, 0, x_19);
 x_21 = lean_alloc_ctor(0, 1, 0);
 lean_ctor_set(x_21, 0, x_20);
-x_22 = l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__2(x_21, x_3, x_4, x_5, x_13);
+x_22 = l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__2(x_21, x_3, x_4, x_5, x_13);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
@@ -1429,7 +1429,7 @@ return x_28;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___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, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___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, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
 _start:
 {
 size_t x_10; size_t x_11; lean_object* x_12; 
@@ -1437,7 +1437,7 @@ x_10 = lean_unbox_usize(x_3);
 lean_dec(x_3);
 x_11 = lean_unbox_usize(x_4);
 lean_dec(x_4);
-x_12 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__1(x_1, x_2, x_10, x_11, x_5, x_6, x_7, x_8, x_9);
+x_12 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__1(x_1, x_2, x_10, x_11, x_5, x_6, x_7, x_8, x_9);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
@@ -1446,11 +1446,11 @@ lean_dec(x_1);
 return x_12;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___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_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 lean_object* x_6; 
-x_6 = l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurence___spec__2(x_1, x_2, x_3, x_4, x_5);
+x_6 = l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___spec__2(x_1, x_2, x_3, x_4, x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
@@ -1519,7 +1519,7 @@ lean_dec(x_3);
 return x_7;
 }
 }
-LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
 uint8_t x_11; 
@@ -1617,7 +1617,7 @@ return x_26;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__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, lean_object* x_7) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__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, lean_object* x_7) {
 _start:
 {
 lean_object* x_8; 
@@ -1625,7 +1625,7 @@ lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
 lean_inc(x_3);
-x_8 = l_Lean_Compiler_LCNF_PassManager_findHighestOccurence(x_1, x_3, x_4, x_5, x_6, x_7);
+x_8 = l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence(x_1, x_3, x_4, x_5, x_6, x_7);
 if (lean_obj_tag(x_8) == 0)
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
@@ -1639,7 +1639,7 @@ x_12 = lean_nat_add(x_9, x_11);
 lean_dec(x_9);
 x_13 = lean_unsigned_to_nat(0u);
 lean_inc(x_12);
-x_14 = l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1___spec__1(x_2, x_12, x_13, x_12, x_11, x_3, x_4, x_5, x_6, x_10);
+x_14 = l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1___spec__1(x_2, x_12, x_13, x_12, x_11, x_3, x_4, x_5, x_6, x_10);
 lean_dec(x_12);
 if (lean_obj_tag(x_14) == 0)
 {
@@ -1715,21 +1715,21 @@ return x_26;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1), 7, 2);
+x_3 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1), 7, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
 lean_object* x_11; 
-x_11 = l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
+x_11 = l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
 lean_dec(x_5);
 lean_dec(x_4);
 return x_11;
@@ -1854,7 +1854,7 @@ static lean_object* _init_l_Lean_Compiler_LCNF_PassInstaller_installAfter___elam
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes(", occurence ", 12);
+x_1 = lean_mk_string_from_bytes(", occurrence ", 13);
 return x_1;
 }
 }
@@ -2049,7 +2049,7 @@ lean_inc(x_1);
 x_3 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_installAfter), 3, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
-x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1), 7, 2);
+x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1), 7, 2);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_3);
 return x_4;
@@ -2157,7 +2157,7 @@ lean_dec(x_5);
 return x_9;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installBeforeEachOccurence(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_installBeforeEachOccurrence(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; 
@@ -2165,7 +2165,7 @@ lean_inc(x_1);
 x_3 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_installBefore), 3, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
-x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1), 7, 2);
+x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1), 7, 2);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_3);
 return x_4;
@@ -2281,7 +2281,7 @@ lean_dec(x_5);
 return x_9;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurence(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurrence(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; 
@@ -2289,7 +2289,7 @@ lean_inc(x_1);
 x_3 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_replacePass), 3, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
-x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurence___elambda__1), 7, 2);
+x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_withEachOccurrence___elambda__1), 7, 2);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_3);
 return x_4;
@@ -3938,8 +3938,8 @@ lean_dec_ref(res);
 l_Lean_Compiler_LCNF_Phase_noConfusion___rarg___closed__1 = _init_l_Lean_Compiler_LCNF_Phase_noConfusion___rarg___closed__1();
 lean_mark_persistent(l_Lean_Compiler_LCNF_Phase_noConfusion___rarg___closed__1);
 l_Lean_Compiler_LCNF_instInhabitedPhase = _init_l_Lean_Compiler_LCNF_instInhabitedPhase();
-l_Lean_Compiler_LCNF_Pass_occurence___default = _init_l_Lean_Compiler_LCNF_Pass_occurence___default();
-lean_mark_persistent(l_Lean_Compiler_LCNF_Pass_occurence___default);
+l_Lean_Compiler_LCNF_Pass_occurrence___default = _init_l_Lean_Compiler_LCNF_Pass_occurrence___default();
+lean_mark_persistent(l_Lean_Compiler_LCNF_Pass_occurrence___default);
 l_Lean_Compiler_LCNF_instInhabitedPass___lambda__1___closed__1 = _init_l_Lean_Compiler_LCNF_instInhabitedPass___lambda__1___closed__1();
 lean_mark_persistent(l_Lean_Compiler_LCNF_instInhabitedPass___lambda__1___closed__1);
 l_Lean_Compiler_LCNF_instInhabitedPass___closed__1 = _init_l_Lean_Compiler_LCNF_instInhabitedPass___closed__1();
@@ -3978,8 +3978,8 @@ l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2_
 lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2___closed__2);
 l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2___closed__3 = _init_l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2___closed__3();
 lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_validate___spec__2___closed__3);
-l_Lean_Compiler_LCNF_PassManager_findHighestOccurence___closed__1 = _init_l_Lean_Compiler_LCNF_PassManager_findHighestOccurence___closed__1();
-lean_mark_persistent(l_Lean_Compiler_LCNF_PassManager_findHighestOccurence___closed__1);
+l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___closed__1 = _init_l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___closed__1();
+lean_mark_persistent(l_Lean_Compiler_LCNF_PassManager_findHighestOccurrence___closed__1);
 l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__1 = _init_l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__1();
 lean_mark_persistent(l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__1);
 l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__2 = _init_l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__2();

stage0/stdlib/Lean/Compiler/LCNF/Passes.c

@@ -29,6 +29,7 @@ static lean_object* l_Lean_Compiler_LCNF_builtin___closed__9;
 static lean_object* l_Lean_Compiler_LCNF_builtin___closed__4;
 extern lean_object* l_Lean_Compiler_LCNF_pullFunDecls;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_builtin;
+static lean_object* l_Lean_Compiler_LCNF_builtin___closed__15;
 static lean_object* l_Lean_Compiler_LCNF_builtin___closed__3;
 lean_object* l_Lean_Compiler_LCNF_PassInstaller_append___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Compiler_LCNF_pullInstances;
@@ -38,6 +39,7 @@ static lean_object* l_Lean_Compiler_LCNF_builtin___closed__7;
 extern lean_object* l_Lean_Compiler_LCNF_cse;
 static lean_object* l_Lean_Compiler_LCNF_builtin___closed__11;
 static lean_object* l_Lean_Compiler_LCNF_builtin___closed__10;
+static lean_object* l_Lean_Compiler_LCNF_builtin___closed__16;
 static lean_object* _init_l_Lean_Compiler_LCNF_builtin___closed__1() {
 _start:
 {
@@ -89,20 +91,20 @@ return x_3;
 static lean_object* _init_l_Lean_Compiler_LCNF_builtin___closed__5() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = lean_unsigned_to_nat(8u);
-x_2 = lean_mk_empty_array_with_capacity(x_1);
-return x_2;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Compiler_LCNF_builtin___closed__1;
+x_2 = lean_unsigned_to_nat(2u);
+x_3 = l_Lean_Compiler_LCNF_simp(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l_Lean_Compiler_LCNF_builtin___closed__6() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Compiler_LCNF_builtin___closed__5;
-x_2 = l_Lean_Compiler_LCNF_pullInstances;
-x_3 = lean_array_push(x_1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_unsigned_to_nat(9u);
+x_2 = lean_mk_empty_array_with_capacity(x_1);
+return x_2;
 }
 }
 static lean_object* _init_l_Lean_Compiler_LCNF_builtin___closed__7() {
@@ -110,7 +112,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__6;
-x_2 = l_Lean_Compiler_LCNF_cse;
+x_2 = l_Lean_Compiler_LCNF_pullInstances;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -120,7 +122,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__7;
-x_2 = l_Lean_Compiler_LCNF_builtin___closed__2;
+x_2 = l_Lean_Compiler_LCNF_cse;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -130,7 +132,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__8;
-x_2 = l_Lean_Compiler_LCNF_pullFunDecls;
+x_2 = l_Lean_Compiler_LCNF_builtin___closed__2;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -140,7 +142,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__9;
-x_2 = l_Lean_Compiler_LCNF_findJoinPoints;
+x_2 = l_Lean_Compiler_LCNF_pullFunDecls;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -150,7 +152,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__10;
-x_2 = l_Lean_Compiler_LCNF_reduceJpArity;
+x_2 = l_Lean_Compiler_LCNF_findJoinPoints;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -160,7 +162,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__11;
-x_2 = l_Lean_Compiler_LCNF_builtin___closed__4;
+x_2 = l_Lean_Compiler_LCNF_reduceJpArity;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -170,7 +172,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__12;
-x_2 = l_Lean_Compiler_LCNF_specialize;
+x_2 = l_Lean_Compiler_LCNF_builtin___closed__4;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@@ -178,8 +180,28 @@ return x_3;
 static lean_object* _init_l_Lean_Compiler_LCNF_builtin___closed__14() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Compiler_LCNF_builtin___closed__13;
+x_2 = l_Lean_Compiler_LCNF_specialize;
+x_3 = lean_array_push(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Compiler_LCNF_builtin___closed__15() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Compiler_LCNF_builtin___closed__14;
+x_2 = l_Lean_Compiler_LCNF_builtin___closed__5;
+x_3 = lean_array_push(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Compiler_LCNF_builtin___closed__16() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_LCNF_builtin___closed__15;
 x_2 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_PassInstaller_append___elambda__1___boxed), 6, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
@@ -189,7 +211,7 @@ static lean_object* _init_l_Lean_Compiler_LCNF_builtin() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Compiler_LCNF_builtin___closed__14;
+x_1 = l_Lean_Compiler_LCNF_builtin___closed__16;
 return x_1;
 }
 }
@@ -262,6 +284,10 @@ l_Lean_Compiler_LCNF_builtin___closed__13 = _init_l_Lean_Compiler_LCNF_builtin__
 lean_mark_persistent(l_Lean_Compiler_LCNF_builtin___closed__13);
 l_Lean_Compiler_LCNF_builtin___closed__14 = _init_l_Lean_Compiler_LCNF_builtin___closed__14();
 lean_mark_persistent(l_Lean_Compiler_LCNF_builtin___closed__14);
+l_Lean_Compiler_LCNF_builtin___closed__15 = _init_l_Lean_Compiler_LCNF_builtin___closed__15();
+lean_mark_persistent(l_Lean_Compiler_LCNF_builtin___closed__15);
+l_Lean_Compiler_LCNF_builtin___closed__16 = _init_l_Lean_Compiler_LCNF_builtin___closed__16();
+lean_mark_persistent(l_Lean_Compiler_LCNF_builtin___closed__16);
 l_Lean_Compiler_LCNF_builtin = _init_l_Lean_Compiler_LCNF_builtin();
 lean_mark_persistent(l_Lean_Compiler_LCNF_builtin);
 return lean_io_result_mk_ok(lean_box(0));

stage0/stdlib/Lean/Compiler/LCNF/SpecInfo.c

@@ -2790,6 +2790,7 @@ lean_dec(x_38);
 x_41 = lean_ctor_get(x_37, 2);
 lean_inc(x_41);
 lean_dec(x_37);
+lean_inc(x_41);
 x_42 = l_Lean_Compiler_LCNF_isArrowClass_x3f(x_41, x_10, x_11, x_39);
 x_43 = lean_ctor_get(x_42, 0);
 lean_inc(x_43);

stage0/stdlib/Lean/Compiler/LCNF/Testing.c

@@ -28,6 +28,7 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Testing_asser
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Testing_assert___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Testing_assertSize___lambda__1___closed__3;
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence(lean_object*, lean_object*, 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_Lean_Compiler_LCNF_Testing_TestM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -37,6 +38,7 @@ lean_object* l_Nat_beq___boxed(lean_object*, lean_object*);
 extern lean_object* l_Std_Format_defWidth;
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAfterTest___elambda__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Testing_assertSize___spec__1___boxed(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___lambda__1(lean_object*, lean_object*, lean_object*, 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_Compiler_LCNF_Testing_assertIsAtFixPoint___lambda__1___closed__3;
 static lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAfterTest___elambda__1___closed__3;
@@ -47,7 +49,6 @@ lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAfterEach(lean_object*, l
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertDoesNotContainConstAfter___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertDoesNotContainConstAfter(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAfterTest___elambda__1___closed__6;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertReducesSize___lambda__1___boxed(lean_object*, lean_object*);
@@ -70,14 +71,13 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Testing_ass
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAfterTest___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfter___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_usize_dec_lt(size_t, size_t);
-lean_object* l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurence(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertPreservesSize(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurrence(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_containsConst___boxed(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Testing_assertReducesSize___closed__1;
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Testing_assert___spec__1___closed__6;
 lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyzeAppStagedCore_maybeSetExplicit___spec__4(lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAroundEachOccurence(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfter___closed__1;
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Testing_assert___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAfterTest___elambda__1___closed__2;
@@ -86,12 +86,9 @@ LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertSize___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_inheritedTraceOptions;
 lean_object* lean_array_fget(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_getPassUnderTest___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Code_containsConst_goExpr___closed__1;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Testing_assertIsAtFixPoint___closed__2;
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Testing_assert___spec__1___closed__4;
@@ -104,6 +101,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertReducesOrPreservesSi
 static lean_object* l_Lean_Compiler_LCNF_Testing_assertIsAtFixPoint___closed__1;
 LEAN_EXPORT uint8_t l_Lean_Compiler_LCNF_Code_containsConst(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAroundTest___elambda__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_getTestName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertNoFun___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -116,6 +114,8 @@ lean_object* l_Nat_repr(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_throwFixPointError(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_format_pretty(lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAroundEachOccurrence(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_LCNF_Testing_assertSize___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAfterTest___elambda__1___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_getInputDecls___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -138,13 +138,14 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertSize(lean_object*, l
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertNoFun___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertSize___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurrence(lean_object*, lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Testing_assert___spec__1___closed__3;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Testing_assertNoFun___spec__4(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_SimpleAssertionM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertIsAtFixPoint(lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_throwFixPointError___closed__2;
 static lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_throwFixPointError___closed__1;
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAfterTest___elambda__1___lambda__2___closed__3;
 lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Testing_assertPreservesSize___closed__1;
@@ -155,7 +156,6 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfter___l
 lean_object* l_Lean_Compiler_LCNF_AltCore_getCode(lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Testing_assert___spec__1___closed__1;
 uint8_t l___private_Lean_Util_Trace_0__Lean_checkTraceOption(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurence(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext(lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfter___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_getDecls___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1212,7 +1212,7 @@ static lean_object* _init_l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compile
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes(" occurence ", 11);
+x_1 = lean_mk_string_from_bytes(" occurrence ", 12);
 return x_1;
 }
 }
@@ -1585,7 +1585,7 @@ lean_closure_set(x_6, 2, x_2);
 return x_6;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurence(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurrence(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; lean_object* x_5; 
@@ -1865,7 +1865,7 @@ lean_dec(x_4);
 return x_10;
 }
 }
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, size_t 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, lean_object* x_13) {
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, size_t 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, lean_object* x_13) {
 _start:
 {
 uint8_t x_14; 
@@ -1948,7 +1948,7 @@ return x_28;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___lambda__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, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___lambda__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, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
 _start:
 {
 lean_object* x_10; lean_object* x_11; uint8_t x_12; 
@@ -2000,28 +2000,28 @@ x_18 = 0;
 x_19 = lean_usize_of_nat(x_10);
 lean_dec(x_10);
 x_20 = lean_box(0);
-x_21 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___spec__1(x_1, x_2, x_3, x_4, x_18, x_19, x_20, x_4, x_5, x_6, x_7, x_8, x_9);
+x_21 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___spec__1(x_1, x_2, x_3, x_4, x_18, x_19, x_20, x_4, x_5, x_6, x_7, x_8, x_9);
 return x_21;
 }
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence(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; 
-x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___lambda__1___boxed), 9, 2);
+x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___lambda__1___boxed), 9, 2);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_2);
 x_5 = l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfter___closed__1;
 x_6 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfter___spec__2___rarg), 8, 2);
 lean_closure_set(x_6, 0, x_5);
 lean_closure_set(x_6, 1, x_4);
-x_7 = l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurence(x_6, x_3);
+x_7 = l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurrence(x_6, x_3);
 return x_7;
 }
 }
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
 _start:
 {
 size_t x_14; size_t x_15; lean_object* x_16; 
@@ -2029,17 +2029,17 @@ x_14 = lean_unbox_usize(x_5);
 lean_dec(x_5);
 x_15 = lean_unbox_usize(x_6);
 lean_dec(x_6);
-x_16 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___spec__1(x_1, x_2, x_3, x_4, x_14, x_15, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
+x_16 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___spec__1(x_1, x_2, x_3, x_4, x_14, x_15, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
 lean_dec(x_8);
 lean_dec(x_4);
 return x_16;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___lambda__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, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___lambda__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, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
 _start:
 {
 lean_object* x_10; 
-x_10 = l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+x_10 = l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
 lean_dec(x_4);
 return x_10;
 }
@@ -2383,7 +2383,7 @@ lean_closure_set(x_6, 2, x_2);
 return x_6;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAroundEachOccurence(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Testing_assertAroundEachOccurrence(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; lean_object* x_5; 
@@ -2392,7 +2392,7 @@ lean_inc(x_3);
 x_4 = lean_alloc_closure((void*)(l___private_Lean_Compiler_LCNF_Testing_0__Lean_Compiler_LCNF_Testing_assertAroundTest), 3, 2);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_2);
-x_5 = l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurence(x_3, x_4);
+x_5 = l_Lean_Compiler_LCNF_PassInstaller_replaceEachOccurrence(x_3, x_4);
 return x_5;
 }
 }
@@ -3139,7 +3139,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; 
 x_2 = l_Lean_Compiler_LCNF_Testing_assertIsAtFixPoint___closed__2;
-x_3 = l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurence(x_2, x_1);
+x_3 = l_Lean_Compiler_LCNF_Testing_assertAfterEachOccurrence(x_2, x_1);
 return x_3;
 }
 }
@@ -3437,7 +3437,7 @@ x_5 = l_Lean_Compiler_LCNF_Testing_assertSize___closed__1;
 x_6 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Compiler_LCNF_Testing_assertSize___spec__3___rarg), 8, 2);
 lean_closure_set(x_6, 0, x_5);
 lean_closure_set(x_6, 1, x_4);
-x_7 = l_Lean_Compiler_LCNF_Testing_assertAroundEachOccurence(x_6, x_3);
+x_7 = l_Lean_Compiler_LCNF_Testing_assertAroundEachOccurrence(x_6, x_3);
 return x_7;
 }
 }
@@ -3593,7 +3593,7 @@ _start:
 lean_object* x_4; lean_object* x_5; 
 x_4 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_Testing_assertDoesNotContainConstAfter___lambda__1___boxed), 3, 1);
 lean_closure_set(x_4, 0, x_1);
-x_5 = l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurence(x_4, x_2, x_3);
+x_5 = l_Lean_Compiler_LCNF_Testing_assertForEachDeclAfterEachOccurrence(x_4, x_2, x_3);
 return x_5;
 }
 }

stage0/stdlib/Lean/Data/Lsp/Capabilities.c

@@ -41,7 +41,7 @@ static lean_object* l_Lean_Lsp_instToJsonTextDocumentClientCapabilities___closed
 static lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_607____closed__4;
 LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonServerCapabilities;
 static lean_object* l_Lean_Lsp_instToJsonCompletionClientCapabilities___closed__1;
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5320_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5317_(lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_workspaceSymbolProvider___default;
 LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_hoverProvider___default;
 lean_object* l_List_join___rarg(lean_object*);
@@ -55,7 +55,7 @@ LEAN_EXPORT lean_object* l_Lean_Lsp_instToJsonCompletionClientCapabilities;
 LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonWindowClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_324____spec__1(lean_object*, lean_object*);
 lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_119_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonTextDocumentClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_191____spec__1(lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5244_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5241_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Lsp_ClientCapabilities_textDocument_x3f___default;
 static lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_607____closed__3;
 LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonTextDocumentClientCapabilities;
@@ -1777,7 +1777,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
 x_4 = lean_ctor_get(x_2, 0);
 lean_inc(x_4);
 lean_dec(x_2);
-x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5320_(x_4);
+x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5317_(x_4);
 x_6 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_6, 0, x_1);
 lean_ctor_set(x_6, 1, x_5);
@@ -2192,7 +2192,7 @@ return x_4;
 else
 {
 lean_object* x_5; 
-x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5244_(x_3);
+x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5241_(x_3);
 lean_dec(x_3);
 if (lean_obj_tag(x_5) == 0)
 {

stage0/stdlib/Lean/Meta/LevelDefEq.c

@@ -2162,7 +2162,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_isLevelMVarAssignable___at_Lean_Meta_isLevelDefEqAuxImpl___spec__2___closed__1;
 x_2 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_isLevelDefEqAuxImpl___spec__2___closed__2;
-x_3 = lean_unsigned_to_nat(365u);
+x_3 = lean_unsigned_to_nat(389u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_isLevelDefEqAuxImpl___spec__2___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

stage0/stdlib/Lean/Meta/SynthInstance.c

@@ -1373,7 +1373,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_isLevelMVarAssignable___at_Lean_Meta_SynthInstance_MkTableKey_normLevel___spec__1___closed__1;
 x_2 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_SynthInstance_MkTableKey_normLevel___spec__1___closed__2;
-x_3 = lean_unsigned_to_nat(365u);
+x_3 = lean_unsigned_to_nat(389u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_SynthInstance_MkTableKey_normLevel___spec__1___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@@ -3429,7 +3429,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_isLevelMVarAssignable___at_Lean_Meta_addImplicitTargets___spec__5___closed__1;
 x_2 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_addImplicitTargets___spec__5___closed__2;
-x_3 = lean_unsigned_to_nat(365u);
+x_3 = lean_unsigned_to_nat(389u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_addImplicitTargets___spec__5___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c

@@ -4012,7 +4012,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_isLevelMVarAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__4___closed__1;
 x_2 = l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__4___closed__2;
-x_3 = lean_unsigned_to_nat(365u);
+x_3 = lean_unsigned_to_nat(389u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__4___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

stage0/stdlib/Lean/MetavarContext.c

@@ -4086,7 +4086,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_isLevelMVarAssignable___rarg___lambda__1___closed__1;
 x_2 = l_Lean_isLevelMVarAssignable___rarg___lambda__1___closed__2;
-x_3 = lean_unsigned_to_nat(365u);
+x_3 = lean_unsigned_to_nat(389u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_isLevelMVarAssignable___rarg___lambda__1___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -4343,7 +4343,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_isLevelMVarAssignable___rarg___lambda__1___closed__1;
 x_2 = l_Lean_MetavarContext_getDecl___closed__1;
-x_3 = lean_unsigned_to_nat(370u);
+x_3 = lean_unsigned_to_nat(394u);
 x_4 = lean_unsigned_to_nat(17u);
 x_5 = l_Lean_MetavarContext_getDecl___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -51895,7 +51895,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_isLevelMVarAssignable___rarg___lambda__1___closed__1;
 x_2 = l_Lean_MetavarContext_getLevelDepth___closed__1;
-x_3 = lean_unsigned_to_nat(810u);
+x_3 = lean_unsigned_to_nat(835u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_MetavarContext_getDecl___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c

@@ -60,7 +60,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight___lamb
 lean_object* lean_array_uget(lean_object*, size_t);
 lean_object* lean_io_error_to_string(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_getInteractiveTermGoal___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1911_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1908_(lean_object*);
 static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__3___closed__7;
 static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__4___lambda__2___closed__1;
 lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonPlainGoalParams____x40_Lean_Data_Lsp_Extra___hyg_516_(lean_object*);
@@ -205,7 +205,7 @@ LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Server_FileWorker_handleSem
 static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__31___lambda__3___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__1___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_map___rarg(lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1809_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1806_(lean_object*);
 lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParams____x40_Lean_Data_Lsp_Extra___hyg_24_(lean_object*);
 static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___closed__3;
 static lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addCommandRange___closed__1;
@@ -248,7 +248,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addRanges(l
 static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___closed__10;
 static lean_object* l_List_mapM_loop___at_Lean_Server_FileWorker_getInteractiveGoals___spec__5___closed__7;
 lean_object* l_Lean_Syntax_findStack_x3f(lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5648_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5645_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__1___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addCommandRange___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
@@ -259,7 +259,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange___rarg___la
 lean_object* l_Lean_Meta_withPPShowLetValuesImp___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_insert___at_Lean_Server_registerLspRequestHandler___spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Widget_InteractiveTermGoal_toInteractiveGoal(lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5692_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5689_(lean_object*);
 lean_object* l_IO_AsyncList_waitAll___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____closed__20;
 LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__10___lambda__1(lean_object*);
@@ -271,7 +271,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight___lamb
 static lean_object* l_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____closed__10;
 static lean_object* l_Lean_Server_FileWorker_handleSemanticTokensFull___rarg___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__3(lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5470_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5467_(lean_object*);
 LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__29___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleSemanticTokensFull(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleSemanticTokens_highlightId___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -303,7 +303,7 @@ static lean_object* l_Lean_Server_FileWorker_noHighlightKinds___closed__12;
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_FileWorker_handlePlainGoal___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_to_list(lean_object*, lean_object*);
 static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__3___closed__3;
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5382_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5379_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handlePlainGoal(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_RefInfo_instCoeRefInfoRefInfo___spec__1(size_t, size_t, lean_object*);
@@ -324,9 +324,9 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleCompletion(lean_object*,
 static lean_object* l_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____closed__12;
 lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_692_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2848_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2845_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_getInteractiveTermGoal___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2800_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2797_(lean_object*);
 lean_object* lean_local_ctx_pop(lean_object*);
 static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__10___lambda__4___closed__1;
 static lean_object* l_List_mapM_loop___at_Lean_Server_FileWorker_getInteractiveGoals___spec__5___closed__5;
@@ -347,7 +347,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Serve
 lean_object* l_Lean_Elab_Info_toElabInfo_x3f(lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDocumentHighlight_highlightReturn_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDocumentHighlight_highlightReturn_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1690_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1687_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__27___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Task_Priority_default;
 lean_object* l_Lean_Elab_Info_range_x3f(lean_object*);
@@ -368,7 +368,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_getInteractiveTermGoal___lambd
 LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__25(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Server_FileWorker_noHighlightKinds___closed__5;
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1639_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1636_(lean_object*);
 static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__3___closed__4;
 static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__21___lambda__2___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addCommandRange(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -554,7 +554,7 @@ static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_Fil
 LEAN_EXPORT lean_object* l_List_spanAux___at_Lean_Server_FileWorker_handleFoldingRange_addRanges___spec__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__26___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Server_FileWorker_handleSemanticTokens___lambda__1(lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5818_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5815_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__7___lambda__1(lean_object*);
 static lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight_highlightReturn_x3f___closed__8;
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -633,7 +633,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight_highli
 LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__16___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDocumentHighlight___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2653_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2650_(lean_object*);
 static lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__2___closed__2;
 static lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__2___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__15(lean_object*);
@@ -16436,7 +16436,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
 _start:
 {
 lean_object* x_2; 
-x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1690_(x_1);
+x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1687_(x_1);
 if (lean_obj_tag(x_2) == 0)
 {
 uint8_t x_3; 
@@ -16592,7 +16592,7 @@ static lean_object* _init_l_Lean_Server_registerLspRequestHandler___at_Lean_Serv
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1639_), 1, 0);
+x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1636_), 1, 0);
 return x_1;
 }
 }
@@ -16889,7 +16889,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
 _start:
 {
 lean_object* x_2; 
-x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1911_(x_1);
+x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1908_(x_1);
 if (lean_obj_tag(x_2) == 0)
 {
 uint8_t x_3; 
@@ -17056,7 +17056,7 @@ lean_object* x_3; lean_object* x_4;
 x_3 = lean_ctor_get(x_1, 0);
 lean_inc(x_3);
 lean_dec(x_1);
-x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1809_(x_3);
+x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1806_(x_3);
 return x_4;
 }
 }
@@ -17854,7 +17854,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
 _start:
 {
 lean_object* x_2; 
-x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2653_(x_1);
+x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2650_(x_1);
 if (lean_obj_tag(x_2) == 0)
 {
 uint8_t x_3; 
@@ -17967,7 +17967,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x
 x_5 = lean_array_uget(x_3, x_2);
 x_6 = lean_unsigned_to_nat(0u);
 x_7 = lean_array_uset(x_3, x_2, x_6);
-x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2800_(x_5);
+x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2797_(x_5);
 x_9 = 1;
 x_10 = lean_usize_add(x_2, x_9);
 x_11 = lean_array_uset(x_7, x_2, x_8);
@@ -18346,7 +18346,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
 _start:
 {
 lean_object* x_2; 
-x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2848_(x_1);
+x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2845_(x_1);
 if (lean_obj_tag(x_2) == 0)
 {
 uint8_t x_3; 
@@ -18804,7 +18804,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
 _start:
 {
 lean_object* x_2; 
-x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5382_(x_1);
+x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5379_(x_1);
 if (lean_obj_tag(x_2) == 0)
 {
 uint8_t x_3; 
@@ -18951,7 +18951,7 @@ static lean_object* _init_l_Lean_Server_registerLspRequestHandler___at_Lean_Serv
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5648_), 1, 0);
+x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5645_), 1, 0);
 return x_1;
 }
 }
@@ -19248,7 +19248,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
 _start:
 {
 lean_object* x_2; 
-x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5470_(x_1);
+x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5467_(x_1);
 if (lean_obj_tag(x_2) == 0)
 {
 uint8_t x_3; 
@@ -19683,7 +19683,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
 _start:
 {
 lean_object* x_2; 
-x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5692_(x_1);
+x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5689_(x_1);
 if (lean_obj_tag(x_2) == 0)
 {
 uint8_t x_3; 
@@ -19796,7 +19796,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x
 x_5 = lean_array_uget(x_3, x_2);
 x_6 = lean_unsigned_to_nat(0u);
 x_7 = lean_array_uset(x_3, x_2, x_6);
-x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5818_(x_5);
+x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5815_(x_5);
 x_9 = 1;
 x_10 = lean_usize_add(x_2, x_9);
 x_11 = lean_array_uset(x_7, x_2, x_8);

stage0/stdlib/Lean/Server/Watchdog.c

@@ -313,7 +313,7 @@ static lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__6;
 lean_object* lean_get_prefix(lean_object*);
 static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__11;
 lean_object* l_Lean_FileMap_ofString(lean_object*);
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3322_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3319_(lean_object*);
 lean_object* l_Std_RBNode_balLeft___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_FileWorker_errorPendingRequests___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_mainLoop(lean_object*, lean_object*, lean_object*);
@@ -532,7 +532,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol(lean_objec
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_IO_FS_Stream_readLspRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__1___closed__1;
 static lean_object* l_Lean_Server_Watchdog_findFileWorker_x21___closed__2;
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2435_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2432_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_References_definitionOf_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_to_int(lean_object*);
@@ -542,7 +542,7 @@ lean_object* l___private_Lean_Data_Lsp_Internal_0__Lean_Lsp_fromJsonLeanIleanInf
 lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_forwardRequestToWorker___closed__1;
 static uint8_t l_Lean_Server_Watchdog_tryWriteMessage___lambda__1___closed__1;
-lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2573_(lean_object*);
+lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2570_(lean_object*);
 LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_Server_Watchdog_forwardRequestToWorker___spec__3(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Server_Watchdog_handleNotification___closed__3;
 lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeResult____x40_Lean_Data_Lsp_InitShutdown___hyg_708_(lean_object*);
@@ -14124,7 +14124,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Wat
 _start:
 {
 lean_object* x_4; 
-x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2573_(x_1);
+x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2570_(x_1);
 if (lean_obj_tag(x_4) == 0)
 {
 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; lean_object* x_13; lean_object* x_14; 
@@ -14173,7 +14173,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x
 x_5 = lean_array_uget(x_3, x_2);
 x_6 = lean_unsigned_to_nat(0u);
 x_7 = lean_array_uset(x_3, x_2, x_6);
-x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3322_(x_5);
+x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3319_(x_5);
 x_9 = 1;
 x_10 = lean_usize_add(x_2, x_9);
 x_11 = lean_array_uset(x_7, x_2, x_8);
@@ -14211,7 +14211,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Wat
 _start:
 {
 lean_object* x_4; 
-x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2435_(x_1);
+x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2432_(x_1);
 if (lean_obj_tag(x_4) == 0)
 {
 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; lean_object* x_13; lean_object* x_14;