chore: update stage0

stage0/src/Init/Prelude.lean

@@ -3244,6 +3244,9 @@ def USize.toUInt64 (u : USize) : UInt64 where
 @[extern "lean_uint64_mix_hash"]
 opaque mixHash (u₁ u₂ : UInt64) : UInt64
 
+instance [Hashable α] {p : α → Prop} : Hashable (Subtype p) where
+  hash a := hash a.val
+
 /-- A opaque string hash function. -/
 @[extern "lean_string_hash"]
 protected opaque String.hash (s : @& String) : UInt64

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

@@ -20,7 +20,7 @@ structure Param where
   fvarId     : FVarId
   binderName : Name
   type       : Expr
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 def Param.toExpr (p : Param) : Expr :=
   .fvar p.fvarId
@@ -36,7 +36,7 @@ structure LetDecl where
   type : Expr
   value : Expr
   pure : Bool
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 structure FunDeclCore (Code : Type) where
   fvarId : FVarId
@@ -70,6 +70,62 @@ abbrev Alt := AltCore Code
 abbrev FunDecl := FunDeclCore Code
 abbrev Cases := CasesCore Code
 
+inductive CodeDecl where
+  | let (decl : LetDecl)
+  | fun (decl : FunDecl)
+  | jp (decl : FunDecl)
+  deriving Inhabited
+
+def CodeDecl.fvarId : CodeDecl → FVarId
+  | .let decl | .fun decl | .jp decl => decl.fvarId
+
+def CodeDecl.isPure : CodeDecl → Bool
+  | .let decl => decl.pure
+  | .fun .. | .jp .. => true
+
+mutual
+  private unsafe def eqImp (c₁ c₂ : Code) : Bool :=
+    if ptrEq c₁ c₂ then
+      true
+    else match c₁, c₂ with
+      | .let d₁ k₁, .let d₂ k₂ => d₁ == d₂ && eqImp k₁ k₂
+      | .fun d₁ k₁, .fun d₂ k₂
+      | .jp d₁ k₁, .jp d₂ k₂ => eqFunDecl d₁ d₂ && eqImp k₁ k₂
+      | .cases c₁, .cases c₂ => eqCases c₁ c₂
+      | .jmp j₁ as₁, .jmp j₂ as₂ => j₁ == j₂ && as₁ == as₂
+      | .return r₁, .return r₂ => r₁ == r₂
+      | .unreach t₁, .unreach t₂ => t₁ == t₂
+      | _, _ => false
+
+  private unsafe def eqFunDecl (d₁ d₂ : FunDecl) : Bool :=
+    if ptrEq d₁ d₂ then
+      true
+    else
+      d₁.fvarId == d₂.fvarId && d₁.binderName == d₂.binderName &&
+      d₁.params == d₂.params && d₁.type == d₂.type &&
+      eqImp d₁.value d₂.value
+
+  private unsafe def eqCases (c₁ c₂ : Cases) : Bool :=
+    c₁.resultType == c₂.resultType && c₁.discr == c₂.discr &&
+    c₁.typeName == c₂.typeName && c₁.alts.isEqv c₂.alts eqAlt
+
+  private unsafe def eqAlt (a₁ a₂ : Alt) : Bool :=
+    match a₁, a₂ with
+    | .default k₁, .default k₂ => eqImp k₁ k₂
+    | .alt c₁ ps₁ k₁, .alt c₂ ps₂ k₂ => c₁ == c₂ && ps₁ == ps₂ && eqImp k₁ k₂
+    | _, _ => false
+end
+
+@[implementedBy eqImp] protected opaque Code.beq : Code → Code → Bool
+
+instance : BEq Code where
+  beq := Code.beq
+
+@[implementedBy eqFunDecl] protected opaque FunDecl.beq : FunDecl → FunDecl → Bool
+
+instance : BEq FunDecl where
+  beq := FunDecl.beq
+
 def AltCore.getCode : Alt → Code
   | .default k => k
   | .alt _ _ k => k
@@ -186,6 +242,15 @@ to be updated.
 -/
 @[implementedBy updateFunDeclCoreImp] opaque FunDeclCore.updateCore (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
+def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
+  let found (i : Nat) := (cases.alts[i]!, { cases with alts := cases.alts.eraseIdx i })
+  if let some i := cases.alts.findIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
+    found i
+  else if let some i := cases.alts.findIdx? fun | .default _ => true | _ => false then
+    found i
+  else
+    unreachable!
+
 def Code.isDecl : Code → Bool
   | .let .. | .fun .. | .jp .. => true
   | _ => false

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

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Compiler.LCNF.InferType
+import Lean.Compiler.LCNF.PrettyPrinter
 
 namespace Lean.Compiler.LCNF
 
@@ -90,11 +91,24 @@ def checkJpInScope (jp : FVarId) : CheckM Unit := do
     -/
     throwError "invalid jump to out of scope join point"
 
+def checkParam (param : Param) : CheckM Unit := do
+  let localDecl ← getLocalDecl param.fvarId
+  unless localDecl.type == param.type do
+    throwError "LCNF parameter mismatch at `{param.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr param.type}"
+
+def checkParams (params : Array Param) : CheckM Unit :=
+  params.forM checkParam
+
 def checkLetDecl (letDecl : LetDecl) : CheckM Unit := do
   checkExpr letDecl.value
   let valueType ← inferType letDecl.value
   unless compatibleTypes letDecl.type valueType do
     throwError "type mismatch at `{letDecl.binderName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr letDecl.type}"
+  let localDecl ← getLocalDecl letDecl.fvarId
+  unless localDecl.type == letDecl.type do
+    throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr letDecl.type}"
+  unless localDecl.value == letDecl.value do
+    throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, value in local context{indentExpr localDecl.value}\nexpected{indentExpr letDecl.value}"
 
 def addFVarId (fvarId : FVarId) : CheckM Unit := do
   if (← get).all.contains fvarId then
@@ -117,27 +131,35 @@ def addFVarId (fvarId : FVarId) : CheckM Unit := do
 mutual
 
 partial def checkFunDeclCore (declName : Name) (type : Expr) (params : Array Param) (value : Code) : CheckM Unit := do
+  checkParams params
   let valueType ← withParams params do
     mkForallParams params (← check value)
   unless compatibleTypes type valueType do
     throwError "type mismatch at `{declName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr type}"
 
-partial def checkFunDecl (funDecl : FunDecl) : CheckM Unit :=
+partial def checkFunDecl (funDecl : FunDecl) : CheckM Unit := do
   checkFunDeclCore funDecl.binderName funDecl.type funDecl.params funDecl.value
+  let localDecl ← getLocalDecl funDecl.fvarId
+  unless localDecl.type == funDecl.type do
+    throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr funDecl.type}"
+  unless (← getFunDecl funDecl.fvarId) == funDecl do
+    throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, declaration in local context does match"
 
 partial def checkCases (c : Cases) : CheckM Expr := do
   let mut ctorNames : NameSet := {}
   let mut hasDefault := false
   checkFVar c.discr
   let discrType ← inferFVarType c.discr
-  let .const declName _ := discrType.headBeta.getAppFn | throwError "unexpected LCNF discriminant type {discrType}"
-  unless c.typeName == declName do
-    throwError "invalid LCNF `{c.typeName}.casesOn`, discriminant has type{indentExpr discrType}"
+  unless discrType.isAnyType do
+    let .const declName _ := discrType.headBeta.getAppFn | throwError "unexpected LCNF discriminant type {discrType}"
+    unless c.typeName == declName do
+      throwError "invalid LCNF `{c.typeName}.casesOn`, discriminant has type{indentExpr discrType}"
   for alt in c.alts do
     let type ←
       match alt with
       | .default k => hasDefault := true; check k
       | .alt ctorName params k =>
+        checkParams params
         if ctorNames.contains ctorName then
           throwError "invalid LCNF `cases`, alternative `{ctorName}` occurs more than once"
         ctorNames := ctorNames.insert ctorName
@@ -180,4 +202,41 @@ end Check
 def Decl.check (decl : Decl) : CompilerM Unit := do
   Check.run do Check.checkFunDeclCore decl.name decl.type decl.params decl.value
 
+/--
+Check whether every local declaration in the local context is used in one of given `decls`.
+-/
+partial def checkDeadLocalDecls (decls : Array Decl) : CompilerM Unit := do
+  let (_, s) := visitDecls decls |>.run {}
+  (← get).lctx.localDecls.forM fun fvarId decl =>
+    unless s.contains fvarId do
+      throwError "LCNF local context contains unused local variable declaration `{decl.userName}`"
+where
+  visitFVar (fvarId : FVarId) : StateM FVarIdHashSet Unit :=
+    modify (·.insert fvarId)
+
+  visitParam (param : Param) : StateM FVarIdHashSet Unit := do
+    visitFVar param.fvarId
+
+  visitParams (params : Array Param) : StateM FVarIdHashSet Unit := do
+    params.forM visitParam
+
+  visitCode (code : Code) : StateM FVarIdHashSet Unit := do
+    match code with
+    | .jmp .. | .return .. | .unreach .. => return ()
+    | .let decl k => visitFVar decl.fvarId; visitCode k
+    | .fun decl k | .jp decl k =>
+      visitFVar decl.fvarId; visitParams decl.params; visitCode decl.value
+      visitCode k
+    | .cases c => c.alts.forM fun alt => do
+      match alt with
+      | .default k => visitCode k
+      | .alt _ ps k => visitParams ps; visitCode k
+
+  visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
+    visitParams decl.params
+    visitCode decl.value
+
+  visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
+    decls.forM visitDecl
+
 end Lean.Compiler.LCNF

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

@@ -45,8 +45,14 @@ def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
 @[inline] def modifyLCtx (f : LCtx → LCtx) : CompilerM Unit := do
    modify fun s => { s with lctx := f s.lctx }
 
-def eraseFVar (fvarId : FVarId) : CompilerM Unit := do
-  modifyLCtx fun lctx => lctx.erase fvarId
+def eraseFVar (fvarId : FVarId) (recursive := true) : CompilerM Unit := do
+  modifyLCtx fun lctx => lctx.erase fvarId recursive
+
+def eraseFVarsAt (code : Code) : CompilerM Unit := do
+  modifyLCtx fun lctx => lctx.eraseFVarsAt code
+
+def eraseParams (params : Array Param) : CompilerM Unit :=
+  params.forM (eraseFVar ·.fvarId)
 
 /--
 A free variable substitution.
@@ -223,6 +229,9 @@ private unsafe def updateLetDeclImp (decl : LetDecl) (type : Expr) (value : Expr
 
 @[implementedBy updateLetDeclImp] opaque LetDecl.update (decl : LetDecl) (type : Expr) (value : Expr) : CompilerM LetDecl
 
+def LetDecl.updateValue (decl : LetDecl) (value : Expr) : CompilerM LetDecl :=
+  decl.update decl.type value
+
 private unsafe def updateFunDeclImp (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl := do
   if ptrEq type decl.type && ptrEq params decl.params && ptrEq value decl.value then
     return decl

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

@@ -34,21 +34,38 @@ def LCtx.eraseLocal (fvarId : FVarId) : LCtx → LCtx
     let localDecls := localDecls.erase fvarId
     { localDecls, funDecls }
 
-partial def LCtx.erase (fvarId : FVarId) : LCtx → LCtx
+partial def LCtx.erase (fvarId : FVarId) (lctx : LCtx) (recursive := true) : LCtx :=
+  match lctx with
   | { localDecls, funDecls } =>
     let localDecls := localDecls.erase fvarId
     match funDecls.find? fvarId with
     | none => { localDecls, funDecls }
     | some funDecl =>
       let funDecls := funDecls.erase fvarId
-      go funDecl.value { localDecls, funDecls }
+      if recursive then
+        go funDecl.value <| goParams funDecl.params { localDecls, funDecls }
+      else
+        { localDecls, funDecls }
 where
+  goParams (params : Array Param) (lctx : LCtx) : LCtx :=
+    params.foldl (init := lctx) fun lctx p => lctx.erase p.fvarId
+
+  goAlts (alts : Array Alt) (lctx : LCtx) : LCtx :=
+    alts.foldl (init := lctx) fun lctx alt =>
+      match alt with
+      | .default k => go k lctx
+      | .alt _ ps k => go k <| goParams ps lctx
+
   go (code : Code) (lctx : LCtx) : LCtx :=
     match code with
     | .let decl k => go k <| lctx.eraseLocal decl.fvarId
     | .jp decl k | .fun decl k => go k <| lctx.erase decl.fvarId
+    | .cases c => goAlts c.alts lctx
     | _ => lctx
 
+def LCtx.eraseFVarsAt (c : Code) (lctx : LCtx) : LCtx :=
+  LCtx.erase.go c lctx
+
 /--
 Convert a LCNF local context into a regular Lean local context.
 -/

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

@@ -49,6 +49,8 @@ def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
         Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl decl}"
       if compiler.check.get (← getOptions) then
         decl.check
+  if compiler.check.get (← getOptions) then
+    checkDeadLocalDecls decls
 
 namespace PassManager
 

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

@@ -101,7 +101,7 @@ structure Context where
 
 structure State where
   /--
-  Free variable substitution. We use it to implement inlining are removing redundant variables `let _x.i := _x.j`
+  Free variable substitution. We use it to implement inlining and removing redundant variables `let _x.i := _x.j`
   -/
   subst : FVarSubst := {}
   /--
@@ -234,63 +234,180 @@ where
     | .jp .. | .jmp .. => false
     | .return .. | .unreach .. => true
 
-def betaReduce (params : Array Param) (code : Code) (args : Array Expr) : SimpM Code := do
+def betaReduce (params : Array Param) (code : Code) (args : Array Expr) (mustInline := false) : SimpM Code := do
   -- TODO: add necessary casts to `args`
   let mut subst := {}
   for param in params, arg in args do
     subst := subst.insert param.fvarId arg
   let code ← code.internalize subst
-  updateFunDeclInfo code
+  updateFunDeclInfo code mustInline
   return code
 
-  /--
-  If `e` is an application that can be inlined, inline it.
+/--
+If `e` is an application that can be inlined, inline it.
 
-  `k?` is the optional "continuation" for `e`, and it may contain loose bound variables
-  that need to instantiated with `xs`. That is, if `k? = some k`, then `k.instantiateRev xs`
-  is an expression without loose bound variables.
-  -/
-  partial def inlineApp? (letDecl : LetDecl) (k : Code) : SimpM (Option Code) := do
-    if k matches .unreach .. then return some k
-    let e := letDecl.value
-    let some info ← inlineCandidate? e | return none
-    markSimplified
-    let args := e.getAppArgs
-    let numArgs := args.size
-    trace[Compiler.simp.inline] "inlining {e}"
-    let code ← betaReduce info.params info.value args[:info.arity]
-    let fvarId := letDecl.fvarId
-    if k.isReturnOf fvarId && numArgs == info.arity then
-      /- Easy case, the continuation `k` is just returning the result of the application. -/
-      return code
-    else if oneExitPointQuick code then
-      /-
-      `code` has only one exit point, thus we can attach the continuation directly there,
-      and simplify the result.
-      -/
-      code.bind fun fvarId' => do
-        /- fvarId' is the result of the computation -/
-        if numArgs > info.arity then
-          let decl ← mkAuxLetDecl (mkAppN (.fvar fvarId') args[info.arity:])
-          let k ← replaceFVar k fvarId decl.fvarId
-          return .let decl k
-        else
-          replaceFVar k fvarId fvarId'
-    else
-      /-
-      `code` has multiple exit points, and the continuation is non-trivial
-      Thus, we create an auxiliary join point.
-      -/
-      let jpParam ← mkAuxParam (← inferType (mkAppN e.getAppFn args[:info.arity]))
-      let jpValue ← if numArgs > info.arity then
-        let decl ← mkAuxLetDecl (mkAppN (.fvar jpParam.fvarId) args[info.arity:])
+`k?` is the optional "continuation" for `e`, and it may contain loose bound variables
+that need to instantiated with `xs`. That is, if `k? = some k`, then `k.instantiateRev xs`
+is an expression without loose bound variables.
+-/
+partial def inlineApp? (letDecl : LetDecl) (k : Code) : SimpM (Option Code) := do
+  if k matches .unreach .. then return some k
+  let e := letDecl.value
+  let some info ← inlineCandidate? e | return none
+  markSimplified
+  let args := e.getAppArgs
+  let numArgs := args.size
+  trace[Compiler.simp.inline] "inlining {e}"
+  let code ← betaReduce info.params info.value args[:info.arity]
+  let fvarId := letDecl.fvarId
+  if k.isReturnOf fvarId && numArgs == info.arity then
+    /- Easy case, the continuation `k` is just returning the result of the application. -/
+    return code
+  else if oneExitPointQuick code then
+    /-
+    `code` has only one exit point, thus we can attach the continuation directly there,
+    and simplify the result.
+    -/
+    code.bind fun fvarId' => do
+      /- fvarId' is the result of the computation -/
+      if numArgs > info.arity then
+        let decl ← mkAuxLetDecl (mkAppN (.fvar fvarId') args[info.arity:])
         let k ← replaceFVar k fvarId decl.fvarId
-        pure <| .let decl k
+        return .let decl k
       else
-        replaceFVar k fvarId jpParam.fvarId
-      let jpDecl ← mkAuxJpDecl #[jpParam] jpValue
-      let code ← code.bind fun fvarId => return .jmp jpDecl.fvarId #[.fvar fvarId]
-      return Code.jp jpDecl code
+        replaceFVar k fvarId fvarId'
+  else
+    /-
+    `code` has multiple exit points, and the continuation is non-trivial
+    Thus, we create an auxiliary join point.
+    -/
+    let jpParam ← mkAuxParam (← inferType (mkAppN e.getAppFn args[:info.arity]))
+    let jpValue ← if numArgs > info.arity then
+      let decl ← mkAuxLetDecl (mkAppN (.fvar jpParam.fvarId) args[info.arity:])
+      let k ← replaceFVar k fvarId decl.fvarId
+      pure <| .let decl k
+    else
+      replaceFVar k fvarId jpParam.fvarId
+    let jpDecl ← mkAuxJpDecl #[jpParam] jpValue
+    let code ← code.bind fun fvarId => return .jmp jpDecl.fvarId #[.fvar fvarId]
+    return Code.jp jpDecl code
+
+/--
+Try to inline a join point.
+-/
+partial def inlineJp? (fvarId : FVarId) (args : Array Expr) : SimpM (Option Code) := do
+  let some decl ← LCNF.findFunDecl? fvarId | return none
+  unless (← shouldInlineLocal decl) do return none
+  betaReduce decl.params decl.value args
+
+def markUsedFVar (fvarId : FVarId) : SimpM Unit :=
+  modify fun s => { s with used := s.used.insert fvarId }
+
+def markUsedExpr (e : Expr) : SimpM Unit :=
+  modify fun s => { s with used := collectLocalDecls s.used e }
+
+def markUsedLetDecl (letDecl : LetDecl) : SimpM Unit :=
+  markUsedExpr letDecl.value
+
+mutual
+partial def markUsedCode (code : Code) : SimpM Unit := do
+  match code with
+  | .let decl k => markUsedLetDecl decl; markUsedCode k
+  | .jp decl k | .fun decl k => markUsedFunDecl decl; markUsedCode k
+  | .return fvarId => markUsedFVar fvarId
+  | .unreach .. => return ()
+  | .jmp fvarId args => markUsedFVar fvarId; args.forM markUsedExpr
+  | .cases c => markUsedFVar c.discr; c.alts.forM fun alt => markUsedCode alt.getCode
+
+partial def markUsedFunDecl (funDecl : FunDecl) : SimpM Unit :=
+  markUsedCode funDecl.value
+end
+
+def isUsed (fvarId : FVarId) : SimpM Bool :=
+  return (← get).used.contains fvarId
+
+def attachCodeDecls (decls : Array CodeDecl) (code : Code) : SimpM Code := do
+  go decls.size code
+where
+  go (i : Nat) (code : Code) : SimpM Code := do
+    if i > 0 then
+      let decl := decls[i-1]!
+      if decl.isPure || (← isUsed decl.fvarId) then
+        match decl with
+        | .let decl => markUsedLetDecl decl; go (i-1) (.let decl code)
+        | .fun decl => markUsedFunDecl decl; go (i-1) (.fun decl code)
+        | .jp decl => markUsedFunDecl decl; go (i-1) (.jp decl code)
+      else
+        eraseFVar decl.fvarId
+        go (i-1) code
+    else
+      return code
+
+def eraseCodeDecls (decls : Array CodeDecl) : SimpM Unit := do
+  decls.forM fun decl => eraseFVar decl.fvarId
+
+/--
+Auxiliary function for projecting "type class dictionary access".
+That is, we are trying to extract one of the type class instance elements.
+Remark: We do not consider parent instances to be elements.
+For example, suppose `e` is `_x_4.1`, and we have
+```
+_x_2 : Monad (ReaderT Bool (ExceptT String Id)) := @ReaderT.Monad Bool (ExceptT String Id) _x_1
+_x_3 : Applicative (ReaderT Bool (ExceptT String Id)) := _x_2.1
+_x_4 : Functor (ReaderT Bool (ExceptT String Id)) := _x_3.1
+```
+Then, we will expand `_x_4.1` since it corresponds to the `Functor` `map` element,
+and its type is not a type class, but is of the form
+```
+{α β : Type u} → (α → β) → ...
+```
+In the example above, the compiler should not expand `_x_3.1` or `_x_2.1` because they are
+type class applications: `Functor` and `Applicative` respectively.
+By eagerly expanding them, we may produce inefficient and bloated code.
+For example, we may be using `_x_3.1` to invoke a function that expects a `Functor` instance.
+By expanding `_x_3.1` we will be just expanding the code that creates this instance.
+
+TODO: explain result
+-/
+partial def inlineProjInst? (e : Expr) : SimpM (Option (Array CodeDecl × FVarId)) := do
+  let .proj _ i s := e | return none
+  let sType ← inferType s
+  unless (← isClass? sType).isSome do return none
+  let eType ← inferType e
+  unless  (← isClass? eType).isNone do return none
+  let (fvarId?, decls) ← visit s [i] |>.run |>.run #[]
+  if let some fvarId := fvarId? then
+    return some (decls, fvarId)
+  else
+    eraseCodeDecls decls
+    return none
+where
+  visit (e : Expr) (projs : List Nat) : OptionT (StateRefT (Array CodeDecl) SimpM) FVarId := do
+    let e ← findExpr e
+    if let .proj _ i s := e then
+      visit s (i :: projs)
+    else if let some (ctorVal, ctorArgs) := e.constructorApp? (← getEnv) then
+      let i :: projs := projs | unreachable!
+      let e := ctorArgs[ctorVal.numParams + i]!
+      if projs.isEmpty then
+        let .fvar fvarId := e | unreachable!
+        return fvarId
+      else
+        visit e projs
+    else
+      let .const declName us := e.getAppFn | failure
+      let some decl ← getStage1Decl? declName | failure
+      guard (decl.getArity == e.getAppNumArgs)
+      let code := decl.instantiateValueLevelParams us
+      let code ← betaReduce decl.params code e.getAppArgs (mustInline := true)
+      visitCode code projs
+
+  visitCode (code : Code) (projs : List Nat) : OptionT (StateRefT (Array CodeDecl) SimpM) FVarId := do
+    match code with
+    | .let decl k => modify (·.push (.let decl)); visitCode k projs
+    | .fun decl k => modify (·.push (.fun decl)); visitCode k projs
+    | .return fvarId => visit (.fvar fvarId) projs
+    | _ => failure
 
 def findCtor (e : Expr) : SimpM Expr := do
   -- TODO: add support for mapping discriminants to constructors in branches
@@ -323,18 +440,6 @@ def simpAppApp? (e : Expr) : OptionT SimpM Expr := do
   markSimplified
   return mkAppN f e.getAppArgs
 
-def markUsedFVar (fvarId : FVarId) : SimpM Unit :=
-  modify fun s => { s with used := s.used.insert fvarId }
-
-def markUsedExpr (e : Expr) : SimpM Unit :=
-  modify fun s => { s with used := collectLocalDecls s.used e }
-
-def markUsedLetDecl (letDecl : LetDecl) : SimpM Unit :=
-  markUsedExpr letDecl.value
-
-def isUsed (fvarId : FVarId) : SimpM Bool :=
-  return (← get).used.contains fvarId
-
 def eraseLocalDecl (fvarId : FVarId) : SimpM Unit := do
   eraseFVar fvarId
   markSimplified
@@ -346,6 +451,11 @@ it is a type, type former, or `lcErased`.
 def addSubst (fvarId : FVarId) (val : Expr) : SimpM Unit :=
   modify fun s => { s with subst := s.subst.insert fvarId val }
 
+/-- Try to apply simple simplifications. -/
+def simpValue? (e : Expr) : SimpM (Option Expr) :=
+  -- TODO: more simplifications
+  simpProj? e <|> simpAppApp? e
+
 mutual
 partial def simpFunDecl (decl : FunDecl) : SimpM FunDecl := do
   let type ← normExpr decl.type
@@ -353,11 +463,29 @@ partial def simpFunDecl (decl : FunDecl) : SimpM FunDecl := do
   let value ← simp decl.value
   decl.update type params value
 
+/-- Try to simplify `cases` of `constructor` -/
+partial def simpCasesOnCtor? (cases : Cases) : SimpM (Option Code) := do
+  let discr ← normFVar cases.discr
+  let discrExpr ← findExpr (.fvar discr)
+  let some (ctorVal, ctorArgs) := discrExpr.constructorApp? (← getEnv) | return none
+  let (alt, cases) := cases.extractAlt! ctorVal.name
+  eraseFVarsAt (.cases cases)
+  markSimplified
+  match alt with
+  | .default k => simp k
+  | .alt _ params k =>
+    let fields := ctorArgs[ctorVal.numParams:]
+    for param in params, field in fields do
+      addSubst param.fvarId field
+    let k ← simp k
+    eraseParams params
+    return k
+
 partial def simp (code : Code) : SimpM Code := do
   incVisited
   match code with
   | .let decl k =>
-    let decl ← normLetDecl decl
+    let mut decl ← normLetDecl decl
     if decl.value.isFVar then
       /- Eliminate `let _x_i := _x_j;` -/
       addSubst decl.fvarId decl.value
@@ -366,8 +494,14 @@ partial def simp (code : Code) : SimpM Code := do
     else if let some code ← inlineApp? decl k then
       eraseFVar decl.fvarId
       simp code
+    else if let some (decls, fvarId) ← inlineProjInst? decl.value then
+      addSubst decl.fvarId (.fvar fvarId)
+      eraseLocalDecl decl.fvarId
+      let k ← simp k
+      attachCodeDecls decls k
     else
-      /- TODO: simple value simplifications & inlining -/
+      if let some value ← simpValue? decl.value then
+        decl ← decl.updateValue value
       let k ← simp k
       if !decl.pure || (← isUsed decl.fvarId) then
         markUsedLetDecl decl
@@ -377,17 +511,28 @@ partial def simp (code : Code) : SimpM Code := do
         eraseLocalDecl decl.fvarId
         return k
   | .fun decl k | .jp decl k =>
-    /-
-    Variables in `decl` will be marked as used even if the function is eliminated.
-    Thus, they will only be deleted in the second pass.
-
-    Pontential improvement: if `decl.fvarId` is marked with `once` or `mustInline`, we will probably
-    inline this declaration, and it may be wasteful to simplify it here.
-    The alternative option is to just normalize `decl`, and if used mark all occurring there as used.
-    -/
-    let decl ← simpFunDecl decl
+    let mut decl := decl
+    let toBeInlined ← isOnceOrMustInline decl.fvarId
+    if toBeInlined then
+      /-
+      If the declaration will be inlined, it is wasteful to eagerly simplify it.
+      So, we just normalize it (i.e., apply the substitution to it).
+      -/
+      decl ← normFunDecl decl
+    else
+      /-
+      Note that functions in `decl` will be marked as used even if `decl` is not actually used.
+      They will only be deleted in the next pass.
+      -/
+      decl ← simpFunDecl decl
     let k ← simp k
     if (← isUsed decl.fvarId) then
+      if toBeInlined then
+        /-
+        `decl` was supposed to be inlined, but there are still references to it.
+        Thus, we must all variables in `decl` as used. Recall it was not eagerly simplified.
+        -/
+        markUsedFunDecl decl
       return code.updateFun! decl k
     else
       /- Dead function elimination -/
@@ -400,19 +545,24 @@ partial def simp (code : Code) : SimpM Code := do
   | .unreach type =>
     return code.updateUnreach! (← normExpr type)
   | .jmp fvarId args =>
-    -- TODO: inline join point
     let fvarId ← normFVar fvarId
     let args ← normExprs args
-    markUsedFVar fvarId
-    args.forM markUsedExpr
-    return code.updateJmp! fvarId args
+    if let some code ← inlineJp? fvarId args then
+      simp code
+    else
+      markUsedFVar fvarId
+      args.forM markUsedExpr
+      return code.updateJmp! fvarId args
   | .cases c =>
-    -- TODO: cases simplifications
-    let resultType ← normExpr c.resultType
-    let discr ← normFVar c.discr
-    markUsedFVar discr
-    let alts ← c.alts.mapMonoM fun alt => return alt.updateCode (← simp alt.getCode)
-    return code.updateCases! resultType discr alts
+    if let some k ← simpCasesOnCtor? c then
+      return k
+    else
+      -- TODO: other cases simplifications
+      let discr ← normFVar c.discr
+      let resultType ← normExpr c.resultType
+      markUsedFVar discr
+      let alts ← c.alts.mapMonoM fun alt => return alt.updateCode (← simp alt.getCode)
+      return code.updateCases! resultType discr alts
 
 end
 
@@ -452,93 +602,10 @@ end Lean.Compiler.LCNF
 
 #exit -- TODO: port rest of file
 
-
 namespace Lean.Compiler
 namespace Simp
 
 
-/-
-Ensure binder names are unique, and update local function information.
-If `mustInline = true`, then local functions in `e` are marked with binders of the
-form `_mustInline.<idx>`.
-Remark: we used to store the `mustInline` information in the map `localInfoMap`,
-using a `.mustInline` constructor at `LocalFunInfo`. However, this was incorrect
-because there is no guarantee that we will be able to inline all occurrences of the
-function in the current `simp` step. Since, we recompute `localInfoMap` from scratch
-at the beginning of each compiler pass, the information was being lost.
--/
-
-
-/--
-This function performs the following operations in the given expression in a single pass.
-- Ensure binder names for let-declarations are unique.
-- Update local function information. That is, it updates the map `localInfoMap`.
-- Apply `e.instantiateRev args`.
-
-We use it to "internalize" expressions at startup and when performing inlining.
--/
-def instantiateRevInternalize (e : Expr) (args : Array Expr) (mustInline := false) : SimpM Expr := do
-  let lctx ← getLCtx
-  let nextIdx := (← getThe CompilerM.State).nextIdx
-  let localInfoMap ← modifyGet fun s => (s.localInfoMap, { s with localInfoMap := {} })
-  let (e, { localInfoMap, nextIdx }) := instantiateRevInternalizeCore lctx e args mustInline |>.run { nextIdx, localInfoMap }
-  modifyThe CompilerM.State fun s => { s with nextIdx }
-  modify fun s => { s with localInfoMap }
-  return e
-
-
-def isSmallValue (value : Expr) : SimpM Bool := do
-  lcnfSizeLe value (← read).config.smallThreshold
-
-def shouldInlineLocal (localDecl : LocalDecl) : SimpM Bool := do
-  if (← isOnceOrMustInline localDecl.userName) then
-    return true
-  else
-    isSmallValue localDecl.value
-
-
-/--
-If `e` if a free variable that expands to a valid LCNF terminal `let`-block expression `e'`,
-return `e'`.
--/
-def expandTrivialExpr (e : Expr) : SimpM Expr := do
-  if e.isFVar then
-    let e' ← findExpr e
-    unless e'.isLambda do
-      if e != e' then
-        markSimplified
-        return e'
-  return e
-
-/--
-Given `value` of the form `let x_1 := v_1; ...; let x_n := v_n; e`,
-return `let x_1; ...; let x_n := v_n; let y : type := e; body`.
-
-This methods assumes `type` and `value` do not have loose bound variables.
-
-Remark: `body` may have many loose bound variables, and the loose bound variables > 0
-must be lifted by `n`.
--/
-private def mkFlatLet (y : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool := false) : Expr :=
-  match value with
-  | .letE binderName type value'@(.lam ..) (.bvar 0) nonDep =>
-    /- Easy case that is often generated by `inlineProjInst?` -/
-    .letE binderName type value' body nonDep
-  | _ => go value 0
-where
-  go (value : Expr) (i : Nat) : Expr :=
-    match value with
-    | .letE n t v b d => .letE n t v (go b (i+1)) d
-    | _ => .letE y type value (body.liftLooseBVars 1 i) nonDep
-
-def mkLetUsingScope (e : Expr) : SimpM Expr := do
-  modify fun s => { s with mkLet := s.mkLet + 1 }
-  Compiler.mkLetUsingScope e
-
-def mkLambda (as : Array Expr) (e : Expr) : SimpM Expr := do
-  modify fun s => { s with mkLambda := s.mkLambda + 1 }
-  Compiler.mkLambda as e
-
 /--
 Helper function for simplifying expressions such as
 ```
@@ -579,77 +646,6 @@ private def etaExpand (type : Expr) (value : Expr) : SimpM Expr := do
       let value ← attachJp value k
       mkLambda xs value
 
-/--
-Auxiliary function for projecting "type class dictionary access".
-That is, we are trying to extract one of the type class instance elements.
-Remark: We do not consider parent instances to be elements.
-For example, suppose `e` is `_x_4.1`, and we have
-```
-_x_2 : Monad (ReaderT Bool (ExceptT String Id)) := @ReaderT.Monad Bool (ExceptT String Id) _x_1
-_x_3 : Applicative (ReaderT Bool (ExceptT String Id)) := _x_2.1
-_x_4 : Functor (ReaderT Bool (ExceptT String Id)) := _x_3.1
-```
-Then, we will expand `_x_4.1` since it corresponds to the `Functor` `map` element,
-and its type is not a type class, but is of the form
-```
-{α β : Type u} → (α → β) → ...
-```
-In the example above, the compiler should not expand `_x_3.1` or `_x_2.1` because they are
-type class applications: `Functor` and `Applicative` respectively.
-By eagerly expanding them, we may produce inefficient and bloated code.
-For example, we may be using `_x_3.1` to invoke a function that expects a `Functor` instance.
-By expanding `_x_3.1` we will be just expanding the code that creates this instance.
--/
-partial def inlineProjInst? (e : Expr) : OptionT SimpM Expr := do
-  let .proj _ _ s := e | failure
-  let sType ← inferType s
-  guard (← isClass? sType).isSome
-  let eType ← inferType e
-  guard (← isClass? eType).isNone
-  /-
-  We use `withNewScope` + `mkLetUsingScope` to filter the relevant let-declarations.
-  Recall that we are extracting only one of the type class elements.
-  -/
-  let value ← withNewScope do mkLetUsingScope (← visitProj e)
-  markSimplified
-  let value := simpUsingEtaReduction value
-  let value ← internalize value (mustInline := true)
-  trace[Compiler.simp.projInst] "{e} =>\n{value}"
-  return value
-where
-  visitProj (e : Expr) : OptionT SimpM Expr := do
-    let .proj _ i s := e | unreachable!
-    let s ← visit s
-    if let some (ctorVal, ctorArgs) := s.constructorApp? (← getEnv) then
-      return ctorArgs[ctorVal.numParams + i]!
-    else
-      failure
-
-  visit (e : Expr) : OptionT SimpM Expr := do
-    let e ← findExpr e
-    if e.isConstructorApp (← getEnv) then
-      return e
-    else if e.isProj then
-      /- We may have nested projections as we traverse parent classes. -/
-      visit (← visitProj e)
-    else
-      let .const declName us := e.getAppFn | failure
-      let some decl ← getStage1Decl? declName | failure
-      guard <| decl.getArity == e.getAppNumArgs
-      let value := decl.value.instantiateLevelParams decl.levelParams us
-      let value := value.beta e.getAppArgs
-      /-
-      Here, we just go inside of the let-declaration block without trying to simplify it.
-      Reason: a type class instannce may have many elements, and it does not make sense to simplify
-      all of them when we are extracting only one of them.
-      -/
-      let value ← Compiler.visitLet (m := SimpM) value fun _ value => return value
-      visit value
-
-def betaReduce (e : Expr) (args : Array Expr) : SimpM Expr := do
-  -- TODO: add necessary casts to `args`
-  let result ← instantiateRevInternalize (getLambdaBody e) args
-  return result
 
 /--
 Try "cases on cases" simplification.
@@ -732,23 +728,6 @@ where
     | _ => jpBody
 
 mutual
-/--
-Simplify the given lambda expression.
-If `checkEmptyTypes := true`, then return `fun a_i : t_i => lcUnreachable` if
-`t_i` is the `Empty` type.
--/
-partial def visitLambda (e : Expr) (checkEmptyTypes := false): SimpM Expr :=
-  withNewScope do
-    let (as, e) ← Compiler.visitLambdaCore e
-    if checkEmptyTypes then
-      for a in as do
-        if (← isEmptyType (← inferType a)) then
-          let e := e.instantiateRev as
-          let unreach ← mkLcUnreachable (← inferType e)
-          let r ← mkLambda as unreach
-          return r
-    let e ← mkLetUsingScope (← visitLet e as)
-    mkLambda as e
 
 partial def visitCases (casesInfo : CasesInfo) (e : Expr) : SimpM Expr := do
   let f := e.getAppFn
@@ -771,74 +750,6 @@ partial def visitCases (casesInfo : CasesInfo) (e : Expr) : SimpM Expr := do
       args ← args.modifyM i (visitLambda · (checkEmptyTypes := true))
     return mkAppN f args
 
-
-/-- Try to apply simple simplifications. -/
-partial def simpValue? (e : Expr) : SimpM (Option Expr) :=
-  simpProj? e <|> simpAppApp? e <|> inlineProjInst? e
-
-/--
-Let-declaration basic block visitor. `e` may contain loose bound variables that
-still have to be instantiated with `xs`.
--/
-partial def visitLet (e : Expr) (xs : Array Expr := #[]): SimpM Expr := do
-  modify fun s => { s with visited := s.visited + 1 }
-  match e with
-  | .letE binderName type value body nonDep =>
-    let type := type.instantiateRev xs
-    let mut value := value.instantiateRev xs
-    if value.isLambda then
-      unless (← isOnceOrMustInline binderName) do
-        /-
-        If the local function will be inlined anyway, we don't simplify it here,
-        we do it after its is inlined and we have information about the actual arguments.
-        -/
-        value ← visitLambda value
-        unless isJpBinderName binderName || (← isSmallValue value) do
-          /-
-          This lambda is not going to be inlined. So, we eta-expand it IF it is not a join point.
-          Recall that local function declarations that are not join points will be lambda lifted
-          anyway. Eta-expanding here also creates new simplification opportunities for
-          monadic local functions before we perform the lambda-lifting.
-          For example, consider the local function
-          ```
-          let _x.23 := fun xs body =>
-            ...
-            let _x.29 := StateRefT'.lift _x.24
-            let _x.30 := _x.25 _x.29
-            let _x.31 := fun a => ...
-            ReaderT.bind _x.30 _x.31
-          ```
-          The function applications `StateRefT'.lift` and `ReaderT.bind` are not inlined because
-          they are partially applied. After, we eta-expand this code, it will be reduced at this stage.
-          -/
-          value ← etaExpand type value
-    else if let some value' ← simpValue? value then
-      if value'.isLet then
-        let e := mkFlatLet binderName type value' body nonDep
-        let e ← visitLet e xs
-        return e
-      value := value'
-    if value.isFVar then
-      /- Eliminate `let _x_i := _x_j;` -/
-      markSimplified
-      visitLet body (xs.push value)
-    else if let some e ← inlineApp? value xs body then
-      return e
-    else
-      let x ← mkLetDecl binderName type value nonDep
-      visitLet body (xs.push x)
-  | _ =>
-    let e := e.instantiateRev xs
-    if let some value ← simpValue? e then
-      visitLet value
-    else if let some casesInfo ← isCasesApp? e then
-      visitCases casesInfo e
-    else if let some e ← inlineApp? e #[] none then
-      return e
-    else
-      expandTrivialExpr e
-end
-
 end Simp
 
 end Lean.Compiler

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

@@ -95,6 +95,7 @@ def toDecl (declName : Name) : CompilerM Decl := do
     return (type, value)
   let value ← toLCNF value
   if let .fun decl (.return _) := value then
+    eraseFVar decl.fvarId (recursive := false)
     return { name := declName, params := decl.params, type, value := decl.value, levelParams := info.levelParams }
   else
     return { name := declName, params := #[], type, value, levelParams := info.levelParams }

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

@@ -33,7 +33,7 @@ inductive Element where
   | fun (decl : FunDecl)
   | let (decl : LetDecl)
   | cases (fvarId : FVarId) (cases : Cases)
-  | unreach
+  | unreach (fvarId : FVarId)
   deriving Inhabited
 
 def seqToCode (seq : Array Element) (e : Expr) : CompilerM Code := do
@@ -50,10 +50,18 @@ where
       | .jp decl => go seq (i - 1) (.jp decl c)
       | .fun decl => go seq (i - 1) (.fun decl c)
       | .let decl => go seq (i - 1) (.let decl c)
-      | .unreach => return .unreach (← c.inferType)
+      | .unreach _ =>
+        let type ← c.inferType
+        eraseFVarsAt c
+        seq[:i].forM fun
+          | .let decl | .jp decl | .fun decl => eraseFVar decl.fvarId
+          | .cases _ cs => eraseFVarsAt (.cases cs)
+          | .unreach fvarId => eraseFVar fvarId
+        return .unreach type
       | .cases fvarId cases =>
         if let .return fvarId' := c then
           if fvarId == fvarId' then
+            eraseFVar fvarId
             go seq (i - 1) (.cases cases)
           else
             -- `cases` is dead code
@@ -92,8 +100,9 @@ def pushElement (elem : Element) : M Unit := do
   modify fun s => { s with seq := s.seq.push elem }
 
 def mkUnreachable (type : Expr) : M Expr := do
-  pushElement .unreach
-  return .fvar (← mkAuxParam type).fvarId
+  let p ← mkAuxParam type
+  pushElement (.unreach p.fvarId)
+  return .fvar p.fvarId
 
 def mkAuxLetDecl (e : Expr) (prefixName := `_x) : M Expr := do
   if e.isFVar then

stage0/src/Lean/Elab/Deriving/TypeName.lean

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 import Lean.Elab.Deriving.Basic
-import Bootstrap.Dynamic
 
 namespace Lean.Elab
 open Command Std Parser Term
@@ -15,12 +14,13 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool
     let cinfo ← getConstInfo declName
     unless cinfo.levelParams.isEmpty do
       throwError m!"{mkConst declName} has universe level parameters"
+    let TypeName := mkIdent `TypeName
     elabCommand <| ← withFreshMacroScope `(
-      unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
-      @[implementedBy instImpl] opaque inst : TypeName @$(mkCIdent declName)
-      instance : TypeName @$(mkCIdent declName) := inst
+      unsafe def instImpl : $TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
+      @[implementedBy instImpl] opaque inst : $TypeName @$(mkCIdent declName)
+      instance : $TypeName @$(mkCIdent declName) := inst
     )
   return true
 
 initialize
-  registerDerivingHandler ``TypeName deriveTypeNameInstance
+  registerDerivingHandler `TypeName deriveTypeNameInstance

stage0/src/Lean/Server/AsyncList.lean

@@ -66,31 +66,30 @@ partial def getAll : AsyncList ε α → List α × Option ε
     | Except.error e => ⟨[], some e⟩
 
 /-- Spawns a `Task` waiting on the prefix of elements for which `p` is true. -/
-partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → BaseIO (Task (List α × Option ε))
-  | cons hd tl => do
+partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → Task (List α × Option ε)
+  | cons hd tl =>
     if p hd then
-      let t ← tl.waitAll p
-      return t.map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
+      (tl.waitAll p).map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
     else
-      return Task.pure ⟨[hd], none⟩
-  | nil => return Task.pure ⟨[], none⟩
-  | delayed tl => do
-    BaseIO.bindTask tl fun
-      | Except.ok tl   => tl.waitAll p
-      | Except.error e => return Task.pure ⟨[], some e⟩
+      .pure ⟨[hd], none⟩
+  | nil => .pure ⟨[], none⟩
+  | delayed tl =>
+    tl.bind fun
+      | .ok tl   => tl.waitAll p
+      | .error e => .pure ⟨[], some e⟩
 
 /-- Spawns a `Task` acting like `List.find?` but which will wait for tail evalution
 when necessary to traverse the list. If the tail terminates before a matching element
 is found, the task throws the terminating value. -/
-partial def waitFind? (p : α → Bool) : AsyncList ε α → BaseIO (Task $ Except ε $ Option α)
-  | nil => return Task.pure <| Except.ok none
-  | cons hd tl => do
-    if p hd then return Task.pure <| Except.ok <| some hd
+partial def waitFind? (p : α → Bool) : AsyncList ε α → Task (Except ε (Option α))
+  | nil => .pure <| .ok none
+  | cons hd tl =>
+    if p hd then .pure <| Except.ok <| some hd
     else tl.waitFind? p
-  | delayed tl => do
-    BaseIO.bindTask tl fun
-      | Except.ok tl   => tl.waitFind? p
-      | Except.error e => return Task.pure <| Except.error e
+  | delayed tl =>
+    tl.bind fun
+      | .ok tl   => tl.waitFind? p
+      | .error e => .pure <| .error e
 
 /-- Retrieve the already-computed prefix of the list. If computation has finished with an error, return it as well. -/
 partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε)
@@ -105,7 +104,8 @@ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε
       | Except.error e => pure ⟨[], some e⟩
     else pure ⟨[], none⟩
 
-def waitHead? (as : AsyncList ε α) : BaseIO (Task (Except ε (Option α))) := as.waitFind? (fun _ => true)
+def waitHead? (as : AsyncList ε α) : Task (Except ε (Option α)) :=
+  as.waitFind? fun _ => true
 
 end AsyncList
 

stage0/src/Lean/Server/FileWorker.lean

@@ -280,7 +280,7 @@ section Updates
     let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
     let cancelTk ← CancelToken.new
     -- Wait for at least one snapshot from the old doc, we don't want to unnecessarily re-run `print-paths`
-    let headSnapTask ← oldDoc.cmdSnaps.waitHead?
+    let headSnapTask := oldDoc.cmdSnaps.waitHead?
     let newSnaps ← EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) fun headSnap?? => do
       let headSnap? ← MonadExcept.ofExcept headSnap??
       -- There is always at least one snapshot absent exceptions

stage0/src/Lean/Server/FileWorker/RequestHandling.lean

@@ -254,7 +254,7 @@ partial def handleDocumentSymbol (_ : DocumentSymbolParams)
     : RequestM (RequestTask DocumentSymbolResult) := do
   let doc ← readDoc
   -- bad: we have to wait on elaboration of the entire file before we can report document symbols
-  let t ← doc.cmdSnaps.waitAll
+  let t := doc.cmdSnaps.waitAll
   mapTask t fun (snaps, _) => do
     let mut stxs := snaps.map (·.stx)
     let (syms, _) := toDocumentSymbols doc.meta.text stxs
@@ -331,7 +331,7 @@ partial def handleSemanticTokens (beginPos endPos : String.Pos)
     : RequestM (RequestTask SemanticTokens) := do
   let doc ← readDoc
   let text := doc.meta.text
-  let t ← doc.cmdSnaps.waitAll (·.beginPos < endPos)
+  let t := doc.cmdSnaps.waitAll (·.beginPos < endPos)
   mapTask t fun (snaps, _) =>
     StateT.run' (s := { data := #[], lastLspPos := ⟨0, 0⟩ : SemanticTokensState }) do
       for s in snaps do
@@ -416,7 +416,7 @@ def handleSemanticTokensRange (p : SemanticTokensRangeParams)
 partial def handleFoldingRange (_ : FoldingRangeParams)
   : RequestM (RequestTask (Array FoldingRange)) := do
   let doc ← readDoc
-  let t ← doc.cmdSnaps.waitAll
+  let t := doc.cmdSnaps.waitAll
   mapTask t fun (snaps, _) => do
     let stxs := snaps.map (·.stx)
     let (_, ranges) ← StateT.run (addRanges doc.meta.text [] stxs) #[]
@@ -491,7 +491,7 @@ partial def handleWaitForDiagnostics (p : WaitForDiagnosticsParams)
   let t ← RequestM.asTask waitLoop
   RequestM.bindTask t fun doc? => do
     let doc ← liftExcept doc?
-    let t₁ ← doc.cmdSnaps.waitAll
+    let t₁ := doc.cmdSnaps.waitAll
     return t₁.map fun _ => pure WaitForDiagnostics.mk
 
 builtin_initialize

stage0/src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -98,7 +98,7 @@ def getInteractiveDiagnostics (params : GetInteractiveDiagnosticsParams) : Reque
   let doc ← readDoc
   let rangeEnd := params.lineRange?.map fun range =>
     doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩
-  let t ← doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
+  let t := doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
   pure <| t.map fun (snaps, _) =>
     let diags? := snaps.getLast?.map fun snap =>
       snap.interactiveDiags.toArray.filter fun diag =>

stage0/src/Lean/Server/Requests.lean

@@ -67,6 +67,8 @@ abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m
 /-- Workers execute request handlers in this monad. -/
 abbrev RequestM := ReaderT RequestContext <| EIO RequestError
 
+abbrev RequestTask.pure (a : α) : RequestTask α := .pure (.ok a)
+
 instance : MonadLift IO RequestM where
   monadLift x := do
     match ←  x.toBaseIO with
@@ -120,7 +122,7 @@ def withWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
     (notFoundX : RequestM β)
     (x : Snapshot → RequestM β)
     : RequestM (RequestTask β) := do
-  let findTask ← doc.cmdSnaps.waitFind? p
+  let findTask := doc.cmdSnaps.waitFind? p
   mapTask findTask <| waitFindSnapAux notFoundX x
 
 /-- See `withWaitFindSnap`. -/
@@ -128,7 +130,7 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
     (notFoundX : RequestM (RequestTask β))
     (x : Snapshot → RequestM (RequestTask β))
     : RequestM (RequestTask β) := do
-  let findTask ← doc.cmdSnaps.waitFind? p
+  let findTask := doc.cmdSnaps.waitFind? p
   bindTask findTask <| waitFindSnapAux notFoundX x
 
 /-- Create a task which waits for the snapshot containing `lspPos` and executes `f` with it.

stage0/src/Lean/Server/Rpc/RequestHandling.lean

@@ -23,33 +23,41 @@ builtin_initialize builtinRpcProcedures : IO.Ref (Std.PHashMap Name RpcProcedure
 builtin_initialize userRpcProcedures : MapDeclarationExtension Name ←
   mkMapDeclarationExtension `userRpcProcedures
 
-open RequestM in
-private unsafe def handleRpcCallUnsafe (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
-  let doc ← readDoc
-  let text := doc.meta.text
-  let callPos := text.lspPosToUtf8Pos p.position
-  bindWaitFindSnap doc (fun s => s.endPos >= callPos)
-    (notFoundX := throwThe RequestError
-      { code := JsonRpc.ErrorCode.invalidParams
-        message := s!"Incorrect position '{p.toTextDocumentPositionParams}' in RPC call" })
-    fun snap => do
-      if let some proc := (← builtinRpcProcedures.get).find? p.method then
-        proc.wrapper p.sessionId p.params
-      else if let some procName := userRpcProcedures.find? snap.env p.method then
-        let options := snap.cmdState.scopes.head!.opts
-        let proc : Except _ _ := Lean.Environment.evalConstCheck RpcProcedure snap.env options ``RpcProcedure procName
-        match proc with
-        | Except.ok x => x.wrapper p.sessionId p.params
-        | Except.error e => throwThe RequestError {
-          code := JsonRpc.ErrorCode.internalError
-          message := s!"Failed to evaluate RPC constant '{procName}': {e}" }
-      else
-        throwThe RequestError {
-          code := JsonRpc.ErrorCode.methodNotFound
-          message := s!"No RPC method '{p.method}' bound" }
+private unsafe def evalRpcProcedureUnsafe (env : Environment) (opts : Options) (procName : Name) :
+    Except String RpcProcedure :=
+  env.evalConstCheck RpcProcedure opts ``RpcProcedure procName
 
-@[implementedBy handleRpcCallUnsafe]
-private opaque handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json)
+@[implementedBy evalRpcProcedureUnsafe]
+opaque evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) :
+    Except String RpcProcedure
+
+open RequestM in
+def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
+  -- The imports are finished at this point, because the handleRequest function
+  -- waits for the header.  (Therefore the built-in RPC procedures won't change
+  -- if we wait for further snapshots.)
+  if let some proc := (← builtinRpcProcedures.get).find? p.method then
+    proc.wrapper p.sessionId p.params
+  else
+    let doc ← readDoc
+    let text := doc.meta.text
+    let callPos := text.lspPosToUtf8Pos p.position
+    let throwNotFound := throwThe RequestError
+      { code := .methodNotFound
+        message := s!"No RPC method '{p.method}' found"}
+    bindWaitFindSnap doc (notFoundX := throwNotFound)
+      (fun s => s.endPos >= callPos ||
+        (userRpcProcedures.find? s.env p.method).isSome)
+      fun snap => do
+        if let some procName := userRpcProcedures.find? snap.env p.method then
+          let options := snap.cmdState.scopes.head!.opts
+          match evalRpcProcedure snap.env options procName with
+          | .ok x => x.wrapper p.sessionId p.params
+          | .error e => throwThe RequestError {
+            code := .internalError
+            message := s!"Failed to evaluate RPC constant '{procName}': {e}" }
+        else
+          throwNotFound
 
 builtin_initialize
   registerLspRequestHandler "$/lean/rpc/call" Lsp.RpcCallParams Json handleRpcCall

stage0/src/Lean/Widget/UserWidget.lean

@@ -95,17 +95,20 @@ structure GetWidgetSourceParams where
   pos : Lean.Lsp.Position
   deriving ToJson, FromJson
 
-open Server in
+open Server RequestM in
 @[serverRpcMethod]
-def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) :=
-  RequestM.withWaitFindSnapAtPos args.pos fun snap => do
-    RequestM.runCoreM snap do
-      let env ← getEnv
-      if let some id := widgetSourceRegistry.getState env |>.find? args.hash then
-        let d ← getUserWidgetDefinition id
-        return {sourcetext := d.javascript}
+def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
+  let doc ← readDoc
+  let pos := doc.meta.text.lspPosToUtf8Pos args.pos
+  let notFound := throwThe RequestError ⟨.invalidParams, s!"No registered user-widget with hash {args.hash}"⟩
+  withWaitFindSnap doc (notFoundX := notFound)
+    (fun s => s.endPos >= pos || (widgetSourceRegistry.getState s.env).contains args.hash)
+    fun snap => do
+      if let some id := widgetSourceRegistry.getState snap.env |>.find? args.hash then
+        runCoreM snap do
+          return {sourcetext := (← getUserWidgetDefinition id).javascript}
       else
-        throwThe RequestError ⟨.invalidParams, s!"No registered user-widget with hash {args.hash}"⟩
+        notFound
 
 open Lean Elab
 
@@ -145,7 +148,7 @@ def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsRes
   let doc ← readDoc
   let filemap := doc.meta.text
   let pos := filemap.lspPosToUtf8Pos args
-  withWaitFindSnapAtPos args fun snap => do
+  withWaitFindSnap doc (·.endPos >= pos) (notFoundX := return ⟨∅⟩) fun snap => do
     let env := snap.env
     let ws := widgetInfosAt? filemap snap.infoTree pos
     let ws ← ws.toArray.mapM (fun (w : UserWidgetInfo) => do

stage0/stdlib/Init/Prelude.c

@@ -195,6 +195,7 @@ LEAN_EXPORT lean_object* l_Lean_Macro_Context_currRecDepth___default;
 static lean_object* l_EStateM_instMonadStateOfEStateM___closed__1;
 LEAN_EXPORT lean_object* l_Applicative_seqRight___default(lean_object*);
 LEAN_EXPORT lean_object* l_EStateM_adaptExcept(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_instHashableSubtype(lean_object*);
 lean_object* lean_string_utf8_byte_size(lean_object*);
 LEAN_EXPORT lean_object* l_cond___rarg(uint8_t, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkAtom(lean_object*);
@@ -268,6 +269,7 @@ LEAN_EXPORT uint8_t l_instDecidableEqChar(uint32_t, uint32_t);
 LEAN_EXPORT lean_object* l_ReaderT_instFunctorReaderT(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Name_casesOn___override___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_EStateM_dummyRestore___rarg___boxed(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_instHashableSubtype___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Macro_instMonadQuotationMacroM___lambda__2(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_namedPattern___rarg(lean_object*, lean_object*);
 static lean_object* l_instSubNat___closed__1;
@@ -6991,6 +6993,22 @@ x_6 = lean_box_uint64(x_5);
 return x_6;
 }
 }
+LEAN_EXPORT lean_object* l_instHashableSubtype___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_apply_1(x_1, x_3);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_instHashableSubtype(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_instHashableSubtype___rarg), 3, 0);
+return x_2;
+}
+}
 LEAN_EXPORT lean_object* l_String_hash___boxed(lean_object* x_1) {
 _start:
 {

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

@@ -14,7 +14,6 @@
 extern "C" {
 #endif
 static lean_object* l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___closed__1;
-extern lean_object* l_Lean_Compiler_LCNF_instInhabitedCode;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_add(size_t, size_t);
 lean_object* l_Lean_stringToMessageData(lean_object*);
@@ -45,13 +44,11 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_FunDecl_etaExpand_mkNewParams___bo
 lean_object* l_Lean_Compiler_LCNF_getArrowArity(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Name_quickCmp(lean_object*, lean_object*);
-static lean_object* l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7___closed__1;
 lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__2;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_FunDecl_etaExpand___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Code_bind_go___closed__2;
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Compiler_LCNF_instInhabitedAltCore___rarg(lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__1;
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_isEmpty___rarg(lean_object*);
@@ -73,12 +70,11 @@ lean_object* l_Lean_Compiler_LCNF_joinTypes(lean_object*, lean_object*);
 uint8_t l_Std_RBNode_isRed___rarg(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*);
+lean_object* l_panic___at_Lean_Compiler_LCNF_CasesCore_extractAlt_x21___spec__2(lean_object*);
 LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Compiler_LCNF_Code_bind_go___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*);
 static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__3;
 lean_object* l_Lean_Compiler_LCNF_AltCore_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_panic_fn(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7(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_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_InferType_mkForallParams___spec__1(size_t, size_t, lean_object*);
@@ -3112,24 +3108,6 @@ return x_24;
 }
 }
 }
-static lean_object* _init_l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7___closed__1() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Compiler_LCNF_instInhabitedCode;
-x_2 = l_Lean_Compiler_LCNF_instInhabitedAltCore___rarg(x_1);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; 
-x_2 = l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7___closed__1;
-x_3 = lean_panic_fn(x_2, x_1);
-return x_3;
-}
-}
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_bind_go___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) {
 _start:
 {
@@ -3189,7 +3167,7 @@ if (x_42 == 0)
 {
 lean_object* x_43; lean_object* x_44; 
 x_43 = l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___closed__4;
-x_44 = l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7(x_43);
+x_44 = l_panic___at_Lean_Compiler_LCNF_CasesCore_extractAlt_x21___spec__2(x_43);
 x_10 = x_44;
 goto block_39;
 }
@@ -4522,8 +4500,6 @@ l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__5 = _
 lean_mark_persistent(l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__5);
 l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__6 = _init_l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__6();
 lean_mark_persistent(l_Lean_throwError___at_Lean_Compiler_LCNF_Code_bind_go___spec__4___closed__6);
-l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7___closed__1 = _init_l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7___closed__1();
-lean_mark_persistent(l_panic___at_Lean_Compiler_LCNF_Code_bind_go___spec__7___closed__1);
 l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___closed__1 = _init_l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___closed__1();
 lean_mark_persistent(l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___closed__1);
 l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___closed__2 = _init_l_Lean_Compiler_LCNF_Code_bind_go___lambda__2___closed__2();

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

@@ -82,7 +82,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Array_BasicAux_0__mapMonoMImp_go_
 static lean_object* l_Lean_Compiler_LCNF_CSE_instMonadFVarSubstM___closed__2;
 lean_object* l_Lean_Expr_fvar___override(lean_object*);
 size_t lean_ptr_addr(lean_object*);
-lean_object* l_Lean_Compiler_LCNF_eraseFVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Compiler_LCNF_eraseFVar(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_LCNF_CSE_instMonadFVarSubstM___spec__2(lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Compiler_LCNF_CSE_addEntry___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1216,83 +1216,84 @@ return x_2;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CSE_replaceFVar(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; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
+uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; 
+x_8 = 1;
 lean_inc(x_1);
-x_8 = l_Lean_Compiler_LCNF_eraseFVar(x_1, x_4, x_5, x_6, x_7);
-x_9 = lean_ctor_get(x_8, 1);
-lean_inc(x_9);
-lean_dec(x_8);
-x_10 = lean_st_ref_take(x_3, x_9);
-x_11 = lean_ctor_get(x_10, 0);
-lean_inc(x_11);
-x_12 = lean_ctor_get(x_10, 1);
+x_9 = l_Lean_Compiler_LCNF_eraseFVar(x_1, x_8, x_4, x_5, x_6, x_7);
+x_10 = lean_ctor_get(x_9, 1);
+lean_inc(x_10);
+lean_dec(x_9);
+x_11 = lean_st_ref_take(x_3, x_10);
+x_12 = lean_ctor_get(x_11, 0);
 lean_inc(x_12);
-lean_dec(x_10);
-x_13 = !lean_is_exclusive(x_11);
-if (x_13 == 0)
-{
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; 
-x_14 = lean_ctor_get(x_11, 1);
-x_15 = l_Lean_Expr_fvar___override(x_2);
-x_16 = l_Std_HashMap_insert___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__3(x_14, x_1, x_15);
-lean_ctor_set(x_11, 1, x_16);
-x_17 = lean_st_ref_set(x_3, x_11, x_12);
-x_18 = !lean_is_exclusive(x_17);
-if (x_18 == 0)
-{
-lean_object* x_19; lean_object* x_20; 
-x_19 = lean_ctor_get(x_17, 0);
-lean_dec(x_19);
-x_20 = lean_box(0);
-lean_ctor_set(x_17, 0, x_20);
-return x_17;
-}
-else
-{
-lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-x_21 = lean_ctor_get(x_17, 1);
-lean_inc(x_21);
-lean_dec(x_17);
-x_22 = lean_box(0);
-x_23 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_23, 0, x_22);
-lean_ctor_set(x_23, 1, x_21);
-return x_23;
-}
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_24 = lean_ctor_get(x_11, 0);
-x_25 = lean_ctor_get(x_11, 1);
-lean_inc(x_25);
-lean_inc(x_24);
+x_13 = lean_ctor_get(x_11, 1);
+lean_inc(x_13);
 lean_dec(x_11);
-x_26 = l_Lean_Expr_fvar___override(x_2);
-x_27 = l_Std_HashMap_insert___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__3(x_25, x_1, x_26);
-x_28 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_28, 0, x_24);
-lean_ctor_set(x_28, 1, x_27);
-x_29 = lean_st_ref_set(x_3, x_28, x_12);
-x_30 = lean_ctor_get(x_29, 1);
-lean_inc(x_30);
-if (lean_is_exclusive(x_29)) {
- lean_ctor_release(x_29, 0);
- lean_ctor_release(x_29, 1);
- x_31 = x_29;
-} else {
- lean_dec_ref(x_29);
- x_31 = lean_box(0);
+x_14 = !lean_is_exclusive(x_12);
+if (x_14 == 0)
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; 
+x_15 = lean_ctor_get(x_12, 1);
+x_16 = l_Lean_Expr_fvar___override(x_2);
+x_17 = l_Std_HashMap_insert___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__3(x_15, x_1, x_16);
+lean_ctor_set(x_12, 1, x_17);
+x_18 = lean_st_ref_set(x_3, x_12, x_13);
+x_19 = !lean_is_exclusive(x_18);
+if (x_19 == 0)
+{
+lean_object* x_20; lean_object* x_21; 
+x_20 = lean_ctor_get(x_18, 0);
+lean_dec(x_20);
+x_21 = lean_box(0);
+lean_ctor_set(x_18, 0, x_21);
+return x_18;
 }
-x_32 = lean_box(0);
-if (lean_is_scalar(x_31)) {
- x_33 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_33 = x_31;
+else
+{
+lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_22 = lean_ctor_get(x_18, 1);
+lean_inc(x_22);
+lean_dec(x_18);
+x_23 = lean_box(0);
+x_24 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_24, 0, x_23);
+lean_ctor_set(x_24, 1, x_22);
+return x_24;
 }
-lean_ctor_set(x_33, 0, x_32);
-lean_ctor_set(x_33, 1, x_30);
-return x_33;
+}
+else
+{
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; 
+x_25 = lean_ctor_get(x_12, 0);
+x_26 = lean_ctor_get(x_12, 1);
+lean_inc(x_26);
+lean_inc(x_25);
+lean_dec(x_12);
+x_27 = l_Lean_Expr_fvar___override(x_2);
+x_28 = l_Std_HashMap_insert___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__3(x_26, x_1, x_27);
+x_29 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_29, 0, x_25);
+lean_ctor_set(x_29, 1, x_28);
+x_30 = lean_st_ref_set(x_3, x_29, x_13);
+x_31 = lean_ctor_get(x_30, 1);
+lean_inc(x_31);
+if (lean_is_exclusive(x_30)) {
+ lean_ctor_release(x_30, 0);
+ lean_ctor_release(x_30, 1);
+ x_32 = x_30;
+} else {
+ lean_dec_ref(x_30);
+ x_32 = lean_box(0);
+}
+x_33 = lean_box(0);
+if (lean_is_scalar(x_32)) {
+ x_34 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_34 = x_32;
+}
+lean_ctor_set(x_34, 0, x_33);
+lean_ctor_set(x_34, 1, x_31);
+return x_34;
 }
 }
 }

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

@@ -67,12 +67,13 @@ static lean_object* l_Lean_Compiler_LCNF_getLocalDecl___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_instAddMessageContextCompilerM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Internalize_internalizeFunDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_LCNF_Basic_0__Lean_Compiler_LCNF_updateAltCodeImp(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVarsAt___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at_Lean_Compiler_LCNF_getLocalDecl___spec__2(lean_object*, lean_object*);
 uint8_t lean_usize_dec_lt(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normExprs(lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___spec__2___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_replaceFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Compiler_LCNF_LCtx_erase(lean_object*, lean_object*);
+lean_object* l_Lean_Compiler_LCNF_LCtx_erase(lean_object*, lean_object*, uint8_t);
 LEAN_EXPORT lean_object* l___private_Init_Data_Array_BasicAux_0__mapMonoMImp___at_Lean_Compiler_LCNF_normParams___spec__1(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_instAddMessageContextCompilerM___closed__1;
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Internalize_internalizeCode___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -88,7 +89,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CompilerM_run(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_cleanup___closed__1;
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_getFunDecl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Compiler_LCNF_mkParam___spec__2___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_instAddMessageContextCompilerM___closed__4;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normLetDecl(lean_object*);
@@ -157,7 +158,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFunDeclImp(lean_object*, lean_
 lean_object* l_Lean_Expr_fvar___override(lean_object*);
 size_t lean_ptr_addr(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkFunDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVar(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParam___at_Lean_Compiler_LCNF_normFunDeclImp___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_getLocalDecl___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp___closed__1;
@@ -165,6 +166,7 @@ LEAN_EXPORT lean_object* l_ReaderT_read___at_Lean_Compiler_LCNF_instMonadFVarSub
 static lean_object* l_Lean_Compiler_LCNF_normExprs___at_Lean_Compiler_LCNF_normCodeImp___spec__2___closed__1;
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_refreshBinderName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Std_AssocList_contains___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__4(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LetDecl_updateValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_LCtx_addLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CompilerM_State_nextIdx___default;
 LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__7(lean_object*, lean_object*);
@@ -173,6 +175,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFVar___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkFreshBinderName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFVar(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseParams(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_replace___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__8(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp___closed__2;
 LEAN_EXPORT lean_object* l___private_Init_Data_Array_BasicAux_0__mapMonoMImp___at_Lean_Compiler_LCNF_normExprs___spec__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -180,6 +183,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParam(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkFreshBinderName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext(lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__1;
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_eraseParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMapImp_moveEntries___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__6(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CompilerM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParams(lean_object*);
@@ -191,9 +195,11 @@ LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compil
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMap_insert___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__3(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Compiler_LCNF_mkParam___spec__2(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LetDecl_updateValue___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_getLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_updateParamImp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Compiler_LCNF_LCtx_erase_go(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_normCodeImp___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_cleanup___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -210,6 +216,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normExpr___at_Lean_Compiler_LCNF_n
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkFreshJpName(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkAuxParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_eraseParams___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_mkAuxParam___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Code_internalize___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_proj___override(lean_object*, lean_object*, lean_object*);
@@ -220,6 +227,7 @@ static lean_object* l_Lean_Compiler_LCNF_mkAuxParam___closed__2;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkLetDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_contains___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__4___boxed(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseParams___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_refreshBinderName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMapImp_find_x3f___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___spec__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Internalize_instMonadFVarSubstM;
@@ -241,6 +249,7 @@ LEAN_EXPORT lean_object* l_Lean_mkFreshFVarId___at___private_Lean_Compiler_LCNF_
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normLetDecl___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_getFunDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_getLocalDecl___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVarsAt(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_getLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkFreshId___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_getFunDecl___closed__2;
@@ -1059,7 +1068,96 @@ lean_dec(x_2);
 return x_6;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVar(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_Compiler_LCNF_eraseFVar(lean_object* x_1, uint8_t 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; uint8_t x_10; 
+x_7 = lean_st_ref_take(x_3, x_6);
+x_8 = lean_ctor_get(x_7, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_7, 1);
+lean_inc(x_9);
+lean_dec(x_7);
+x_10 = !lean_is_exclusive(x_8);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; 
+x_11 = lean_ctor_get(x_8, 0);
+x_12 = l_Lean_Compiler_LCNF_LCtx_erase(x_1, x_11, x_2);
+lean_ctor_set(x_8, 0, x_12);
+x_13 = lean_st_ref_set(x_3, x_8, x_9);
+x_14 = !lean_is_exclusive(x_13);
+if (x_14 == 0)
+{
+lean_object* x_15; lean_object* x_16; 
+x_15 = lean_ctor_get(x_13, 0);
+lean_dec(x_15);
+x_16 = lean_box(0);
+lean_ctor_set(x_13, 0, x_16);
+return x_13;
+}
+else
+{
+lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_17 = lean_ctor_get(x_13, 1);
+lean_inc(x_17);
+lean_dec(x_13);
+x_18 = lean_box(0);
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_18);
+lean_ctor_set(x_19, 1, x_17);
+return x_19;
+}
+}
+else
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_20 = lean_ctor_get(x_8, 0);
+x_21 = lean_ctor_get(x_8, 1);
+lean_inc(x_21);
+lean_inc(x_20);
+lean_dec(x_8);
+x_22 = l_Lean_Compiler_LCNF_LCtx_erase(x_1, x_20, x_2);
+x_23 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_23, 0, x_22);
+lean_ctor_set(x_23, 1, x_21);
+x_24 = lean_st_ref_set(x_3, x_23, x_9);
+x_25 = lean_ctor_get(x_24, 1);
+lean_inc(x_25);
+if (lean_is_exclusive(x_24)) {
+ lean_ctor_release(x_24, 0);
+ lean_ctor_release(x_24, 1);
+ x_26 = x_24;
+} else {
+ lean_dec_ref(x_24);
+ x_26 = lean_box(0);
+}
+x_27 = lean_box(0);
+if (lean_is_scalar(x_26)) {
+ x_28 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_28 = x_26;
+}
+lean_ctor_set(x_28, 0, x_27);
+lean_ctor_set(x_28, 1, x_25);
+return x_28;
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVar___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+uint8_t x_7; lean_object* x_8; 
+x_7 = lean_unbox(x_2);
+lean_dec(x_2);
+x_8 = l_Lean_Compiler_LCNF_eraseFVar(x_1, x_7, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+return x_8;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVarsAt(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; uint8_t x_9; 
@@ -1074,7 +1172,7 @@ if (x_9 == 0)
 {
 lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
 x_10 = lean_ctor_get(x_7, 0);
-x_11 = l_Lean_Compiler_LCNF_LCtx_erase(x_1, x_10);
+x_11 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_1, x_10);
 lean_ctor_set(x_7, 0, x_11);
 x_12 = lean_st_ref_set(x_2, x_7, x_8);
 x_13 = !lean_is_exclusive(x_12);
@@ -1108,7 +1206,7 @@ x_20 = lean_ctor_get(x_7, 1);
 lean_inc(x_20);
 lean_inc(x_19);
 lean_dec(x_7);
-x_21 = l_Lean_Compiler_LCNF_LCtx_erase(x_1, x_19);
+x_21 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_1, x_19);
 x_22 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_22, 0, x_21);
 lean_ctor_set(x_22, 1, x_20);
@@ -1135,17 +1233,132 @@ return x_27;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseFVar___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_Compiler_LCNF_eraseFVarsAt___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_Compiler_LCNF_eraseFVar(x_1, x_2, x_3, x_4, x_5);
+x_6 = l_Lean_Compiler_LCNF_eraseFVarsAt(x_1, x_2, x_3, x_4, x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 return x_6;
 }
 }
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_eraseParams___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+_start:
+{
+uint8_t x_9; 
+x_9 = lean_usize_dec_eq(x_2, x_3);
+if (x_9 == 0)
+{
+lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; size_t x_16; size_t x_17; 
+lean_dec(x_4);
+x_10 = lean_array_uget(x_1, x_2);
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
+lean_dec(x_10);
+x_12 = 1;
+x_13 = l_Lean_Compiler_LCNF_eraseFVar(x_11, x_12, x_5, x_6, x_7, x_8);
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
+x_16 = 1;
+x_17 = lean_usize_add(x_2, x_16);
+x_2 = x_17;
+x_4 = x_14;
+x_8 = x_15;
+goto _start;
+}
+else
+{
+lean_object* x_19; 
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_4);
+lean_ctor_set(x_19, 1, x_8);
+return x_19;
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseParams(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; uint8_t x_8; 
+x_6 = lean_array_get_size(x_1);
+x_7 = lean_unsigned_to_nat(0u);
+x_8 = lean_nat_dec_lt(x_7, x_6);
+if (x_8 == 0)
+{
+lean_object* x_9; lean_object* x_10; 
+lean_dec(x_6);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+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_5);
+return x_10;
+}
+else
+{
+uint8_t x_11; 
+x_11 = lean_nat_dec_le(x_6, x_6);
+if (x_11 == 0)
+{
+lean_object* x_12; lean_object* x_13; 
+lean_dec(x_6);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_12 = lean_box(0);
+x_13 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_13, 0, x_12);
+lean_ctor_set(x_13, 1, x_5);
+return x_13;
+}
+else
+{
+size_t x_14; size_t x_15; lean_object* x_16; lean_object* x_17; 
+x_14 = 0;
+x_15 = lean_usize_of_nat(x_6);
+lean_dec(x_6);
+x_16 = lean_box(0);
+x_17 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_eraseParams___spec__1(x_1, x_14, x_15, x_16, x_2, x_3, x_4, x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_17;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_eraseParams___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) {
+_start:
+{
+size_t x_9; size_t x_10; lean_object* x_11; 
+x_9 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_10 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_11 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_eraseParams___spec__1(x_1, x_9, x_10, x_4, x_5, x_6, x_7, x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_1);
+return x_11;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseParams___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_Compiler_LCNF_eraseParams(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_1);
+return x_6;
+}
+}
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___spec__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -1228,7 +1441,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___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__1;
 x_2 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__2;
-x_3 = lean_unsigned_to_nat(74u);
+x_3 = lean_unsigned_to_nat(80u);
 x_4 = lean_unsigned_to_nat(20u);
 x_5 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -1563,7 +1776,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___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__1;
 x_2 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp___closed__1;
-x_3 = lean_unsigned_to_nat(81u);
+x_3 = lean_unsigned_to_nat(87u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -5538,6 +5751,27 @@ lean_dec(x_4);
 return x_8;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LetDecl_updateValue(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; 
+x_7 = lean_ctor_get(x_1, 2);
+lean_inc(x_7);
+x_8 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_updateLetDeclImp(x_1, x_7, x_2, x_3, x_4, x_5, x_6);
+return x_8;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LetDecl_updateValue___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_Compiler_LCNF_LetDecl_updateValue(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+return x_7;
+}
+}
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_updateFunDeclImp(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) {
 _start:
 {

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

@@ -18,6 +18,7 @@ LEAN_EXPORT lean_object* l_Std_AssocList_replace___at_Lean_Compiler_LCNF_LCtx_ad
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_erase___at_Lean_Compiler_LCNF_LCtx_eraseLocal___spec__2___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Compiler_LCNF_LCtx_localDecls___default___spec__1___boxed(lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goAlts___spec__1(lean_object*, size_t, size_t, lean_object*);
 uint8_t lean_usize_dec_eq(size_t, size_t);
 lean_object* lean_array_uget(lean_object*, size_t);
 uint64_t l___private_Lean_Expr_0__Lean_hashFVarId____x40_Lean_Expr___hyg_1681_(lean_object*);
@@ -42,9 +43,10 @@ static lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext___closed__7;
 uint8_t lean_usize_dec_lt(size_t, size_t);
 static lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext___closed__1;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_LCtx_toLocalContext___spec__4(lean_object*, size_t, size_t, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase(lean_object*, lean_object*, uint8_t);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Std_AssocList_contains___at_Lean_Compiler_LCNF_LCtx_addLocalDecl___spec__2(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_eraseFVarsAt(lean_object*, lean_object*);
 size_t lean_uint64_to_usize(uint64_t);
 LEAN_EXPORT lean_object* l_Std_AssocList_erase___at_Lean_Compiler_LCNF_LCtx_erase___spec__4___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_replace___at_Lean_Compiler_LCNF_LCtx_addFunDecl___spec__6(lean_object*, lean_object*, lean_object*);
@@ -52,9 +54,11 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_
 lean_object* lean_array_fget(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_localDecls___default;
 LEAN_EXPORT lean_object* l_Std_HashMap_toArray___at_Lean_Compiler_LCNF_LCtx_toLocalContext___spec__1(lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goParams___spec__1(lean_object*, size_t, size_t, lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_contains___at_Lean_Compiler_LCNF_LCtx_addFunDecl___spec__2___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_funDecls___default;
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goParams(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at_Lean_Compiler_LCNF_LCtx_addLocalDecl___spec__5(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMap_insert___at_Lean_Compiler_LCNF_LCtx_addLocalDecl___spec__1(lean_object*, lean_object*, lean_object*);
@@ -63,6 +67,7 @@ lean_object* l_Std_mkHashMapImp___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_toLocalContext___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at_Lean_Compiler_LCNF_LCtx_addLocalDecl___spec__3(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext___closed__5;
 LEAN_EXPORT lean_object* l_Std_AssocList_erase___at_Lean_Compiler_LCNF_LCtx_erase___spec__4(lean_object*, lean_object*);
 size_t lean_usize_modn(size_t, lean_object*);
@@ -80,6 +85,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext(lean_object*);
 lean_object* l_Lean_LocalContext_addDecl(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_erase___at_Lean_Compiler_LCNF_LCtx_eraseLocal___spec__2(lean_object*, lean_object*);
 lean_object* lean_nat_mul(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Compiler_LCNF_LCtx_localDecls___default___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__2(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext___closed__2;
@@ -89,12 +95,16 @@ static lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext___closed__4;
 LEAN_EXPORT uint8_t l_Std_AssocList_contains___at_Lean_Compiler_LCNF_LCtx_addFunDecl___spec__2(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at_Lean_Compiler_LCNF_LCtx_addFunDecl___spec__3(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_LCtx_toLocalContext___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goAlts___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Std_HashMap_toArray___at_Lean_Compiler_LCNF_LCtx_toLocalContext___spec__1___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_addFunDecl(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__2___boxed(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goAlts(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext___closed__6;
 LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Compiler_LCNF_LCtx_funDecls___default___spec__1(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goAlts___boxed(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goParams___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Compiler_LCNF_LCtx_localDecls___default___spec__1(lean_object* x_1) {
 _start:
 {
@@ -1147,64 +1157,62 @@ lean_dec(x_1);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_go(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goParams___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
 _start:
 {
-switch (lean_obj_tag(x_1)) {
-case 0:
+uint8_t x_5; 
+x_5 = lean_usize_dec_eq(x_2, x_3);
+if (x_5 == 0)
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_3 = lean_ctor_get(x_1, 0);
-lean_inc(x_3);
-x_4 = lean_ctor_get(x_1, 1);
-lean_inc(x_4);
-lean_dec(x_1);
-x_5 = lean_ctor_get(x_3, 0);
-lean_inc(x_5);
-lean_dec(x_3);
-x_6 = l_Lean_Compiler_LCNF_LCtx_eraseLocal(x_5, x_2);
-lean_dec(x_5);
-x_1 = x_4;
-x_2 = x_6;
-goto _start;
-}
-case 1:
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_8 = lean_ctor_get(x_1, 0);
-lean_inc(x_8);
-x_9 = lean_ctor_get(x_1, 1);
-lean_inc(x_9);
-lean_dec(x_1);
-x_10 = lean_ctor_get(x_8, 0);
-lean_inc(x_10);
-lean_dec(x_8);
-x_11 = l_Lean_Compiler_LCNF_LCtx_erase(x_10, x_2);
-x_1 = x_9;
+lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; size_t x_10; size_t x_11; 
+x_6 = lean_array_uget(x_1, x_2);
+x_7 = lean_ctor_get(x_6, 0);
+lean_inc(x_7);
+lean_dec(x_6);
+x_8 = 1;
+x_9 = l_Lean_Compiler_LCNF_LCtx_erase(x_7, x_4, x_8);
+x_10 = 1;
+x_11 = lean_usize_add(x_2, x_10);
 x_2 = x_11;
+x_4 = x_9;
 goto _start;
 }
-case 2:
+else
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_13 = lean_ctor_get(x_1, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_1, 1);
-lean_inc(x_14);
-lean_dec(x_1);
-x_15 = lean_ctor_get(x_13, 0);
-lean_inc(x_15);
-lean_dec(x_13);
-x_16 = l_Lean_Compiler_LCNF_LCtx_erase(x_15, x_2);
-x_1 = x_14;
-x_2 = x_16;
-goto _start;
+return x_4;
 }
-default: 
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goParams(lean_object* x_1, lean_object* x_2) {
+_start:
 {
-lean_dec(x_1);
+lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_3 = lean_array_get_size(x_1);
+x_4 = lean_unsigned_to_nat(0u);
+x_5 = lean_nat_dec_lt(x_4, x_3);
+if (x_5 == 0)
+{
+lean_dec(x_3);
 return x_2;
 }
+else
+{
+uint8_t x_6; 
+x_6 = lean_nat_dec_le(x_3, x_3);
+if (x_6 == 0)
+{
+lean_dec(x_3);
+return x_2;
+}
+else
+{
+size_t x_7; size_t x_8; lean_object* x_9; 
+x_7 = 0;
+x_8 = lean_usize_of_nat(x_3);
+lean_dec(x_3);
+x_9 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goParams___spec__1(x_1, x_7, x_8, x_2);
+return x_9;
+}
 }
 }
 }
@@ -1385,84 +1393,291 @@ return x_22;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase(lean_object* x_1, lean_object* x_2, uint8_t x_3) {
 _start:
 {
-uint8_t x_3; 
-x_3 = !lean_is_exclusive(x_2);
-if (x_3 == 0)
+uint8_t x_4; 
+x_4 = !lean_is_exclusive(x_2);
+if (x_4 == 0)
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-x_4 = lean_ctor_get(x_2, 0);
-x_5 = lean_ctor_get(x_2, 1);
-x_6 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_eraseLocal___spec__1(x_4, x_1);
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_5 = lean_ctor_get(x_2, 0);
+x_6 = lean_ctor_get(x_2, 1);
+x_7 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_eraseLocal___spec__1(x_5, x_1);
 lean_inc(x_1);
-lean_inc(x_5);
-x_7 = l_Std_HashMapImp_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__1(x_5, x_1);
-if (lean_obj_tag(x_7) == 0)
+lean_inc(x_6);
+x_8 = l_Std_HashMapImp_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__1(x_6, x_1);
+if (lean_obj_tag(x_8) == 0)
 {
 lean_dec(x_1);
-lean_ctor_set(x_2, 0, x_6);
+lean_ctor_set(x_2, 0, x_7);
 return x_2;
 }
 else
 {
-lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_8 = lean_ctor_get(x_7, 0);
-lean_inc(x_8);
-lean_dec(x_7);
-x_9 = lean_ctor_get(x_8, 4);
+lean_object* x_9; lean_object* x_10; 
+x_9 = lean_ctor_get(x_8, 0);
 lean_inc(x_9);
 lean_dec(x_8);
-x_10 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_erase___spec__3(x_5, x_1);
+x_10 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_erase___spec__3(x_6, x_1);
 lean_dec(x_1);
+if (x_3 == 0)
+{
+lean_dec(x_9);
 lean_ctor_set(x_2, 1, x_10);
-lean_ctor_set(x_2, 0, x_6);
-x_11 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_9, x_2);
-return x_11;
-}
+lean_ctor_set(x_2, 0, x_7);
+return x_2;
 }
 else
 {
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_12 = lean_ctor_get(x_2, 0);
-x_13 = lean_ctor_get(x_2, 1);
-lean_inc(x_13);
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_11 = lean_ctor_get(x_9, 4);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_9, 2);
 lean_inc(x_12);
-lean_dec(x_2);
-x_14 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_eraseLocal___spec__1(x_12, x_1);
-lean_inc(x_1);
-lean_inc(x_13);
-x_15 = l_Std_HashMapImp_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__1(x_13, x_1);
-if (lean_obj_tag(x_15) == 0)
-{
-lean_object* x_16; 
-lean_dec(x_1);
-x_16 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_16, 0, x_14);
-lean_ctor_set(x_16, 1, x_13);
-return x_16;
+lean_dec(x_9);
+lean_ctor_set(x_2, 1, x_10);
+lean_ctor_set(x_2, 0, x_7);
+x_13 = l_Lean_Compiler_LCNF_LCtx_erase_goParams(x_12, x_2);
+lean_dec(x_12);
+x_14 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_11, x_13);
+return x_14;
+}
+}
 }
 else
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_17 = lean_ctor_get(x_15, 0);
-lean_inc(x_17);
-lean_dec(x_15);
-x_18 = lean_ctor_get(x_17, 4);
-lean_inc(x_18);
-lean_dec(x_17);
-x_19 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_erase___spec__3(x_13, x_1);
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_15 = lean_ctor_get(x_2, 0);
+x_16 = lean_ctor_get(x_2, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_2);
+x_17 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_eraseLocal___spec__1(x_15, x_1);
+lean_inc(x_1);
+lean_inc(x_16);
+x_18 = l_Std_HashMapImp_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__1(x_16, x_1);
+if (lean_obj_tag(x_18) == 0)
+{
+lean_object* x_19; 
 lean_dec(x_1);
-x_20 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_20, 0, x_14);
-lean_ctor_set(x_20, 1, x_19);
-x_21 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_18, x_20);
-return x_21;
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_17);
+lean_ctor_set(x_19, 1, x_16);
+return x_19;
+}
+else
+{
+lean_object* x_20; lean_object* x_21; 
+x_20 = lean_ctor_get(x_18, 0);
+lean_inc(x_20);
+lean_dec(x_18);
+x_21 = l_Std_HashMapImp_erase___at_Lean_Compiler_LCNF_LCtx_erase___spec__3(x_16, x_1);
+lean_dec(x_1);
+if (x_3 == 0)
+{
+lean_object* x_22; 
+lean_dec(x_20);
+x_22 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_22, 0, x_17);
+lean_ctor_set(x_22, 1, x_21);
+return x_22;
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_23 = lean_ctor_get(x_20, 4);
+lean_inc(x_23);
+x_24 = lean_ctor_get(x_20, 2);
+lean_inc(x_24);
+lean_dec(x_20);
+x_25 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_25, 0, x_17);
+lean_ctor_set(x_25, 1, x_21);
+x_26 = l_Lean_Compiler_LCNF_LCtx_erase_goParams(x_24, x_25);
+lean_dec(x_24);
+x_27 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_23, x_26);
+return x_27;
 }
 }
 }
 }
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_go(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+switch (lean_obj_tag(x_1)) {
+case 0:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_3 = lean_ctor_get(x_1, 0);
+lean_inc(x_3);
+x_4 = lean_ctor_get(x_1, 1);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_ctor_get(x_3, 0);
+lean_inc(x_5);
+lean_dec(x_3);
+x_6 = l_Lean_Compiler_LCNF_LCtx_eraseLocal(x_5, x_2);
+lean_dec(x_5);
+x_1 = x_4;
+x_2 = x_6;
+goto _start;
+}
+case 1:
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; 
+x_8 = lean_ctor_get(x_1, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_1, 1);
+lean_inc(x_9);
+lean_dec(x_1);
+x_10 = lean_ctor_get(x_8, 0);
+lean_inc(x_10);
+lean_dec(x_8);
+x_11 = 1;
+x_12 = l_Lean_Compiler_LCNF_LCtx_erase(x_10, x_2, x_11);
+x_1 = x_9;
+x_2 = x_12;
+goto _start;
+}
+case 2:
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18; 
+x_14 = lean_ctor_get(x_1, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_1, 1);
+lean_inc(x_15);
+lean_dec(x_1);
+x_16 = lean_ctor_get(x_14, 0);
+lean_inc(x_16);
+lean_dec(x_14);
+x_17 = 1;
+x_18 = l_Lean_Compiler_LCNF_LCtx_erase(x_16, x_2, x_17);
+x_1 = x_15;
+x_2 = x_18;
+goto _start;
+}
+case 4:
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_20 = lean_ctor_get(x_1, 0);
+lean_inc(x_20);
+lean_dec(x_1);
+x_21 = lean_ctor_get(x_20, 3);
+lean_inc(x_21);
+lean_dec(x_20);
+x_22 = l_Lean_Compiler_LCNF_LCtx_erase_goAlts(x_21, x_2);
+lean_dec(x_21);
+return x_22;
+}
+default: 
+{
+lean_dec(x_1);
+return x_2;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goAlts___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
+_start:
+{
+uint8_t x_5; 
+x_5 = lean_usize_dec_eq(x_2, x_3);
+if (x_5 == 0)
+{
+lean_object* x_6; size_t x_7; size_t x_8; 
+x_6 = lean_array_uget(x_1, x_2);
+x_7 = 1;
+x_8 = lean_usize_add(x_2, x_7);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_9 = lean_ctor_get(x_6, 1);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_6, 2);
+lean_inc(x_10);
+lean_dec(x_6);
+x_11 = l_Lean_Compiler_LCNF_LCtx_erase_goParams(x_9, x_4);
+lean_dec(x_9);
+x_12 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_10, x_11);
+x_2 = x_8;
+x_4 = x_12;
+goto _start;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; 
+x_14 = lean_ctor_get(x_6, 0);
+lean_inc(x_14);
+lean_dec(x_6);
+x_15 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_14, x_4);
+x_2 = x_8;
+x_4 = x_15;
+goto _start;
+}
+}
+else
+{
+return x_4;
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goAlts(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_3 = lean_array_get_size(x_1);
+x_4 = lean_unsigned_to_nat(0u);
+x_5 = lean_nat_dec_lt(x_4, x_3);
+if (x_5 == 0)
+{
+lean_dec(x_3);
+return x_2;
+}
+else
+{
+uint8_t x_6; 
+x_6 = lean_nat_dec_le(x_3, x_3);
+if (x_6 == 0)
+{
+lean_dec(x_3);
+return x_2;
+}
+else
+{
+size_t x_7; size_t x_8; lean_object* x_9; 
+x_7 = 0;
+x_8 = lean_usize_of_nat(x_3);
+lean_dec(x_3);
+x_9 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goAlts___spec__1(x_1, x_7, x_8, x_2);
+return x_9;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goParams___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+size_t x_5; size_t x_6; lean_object* x_7; 
+x_5 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_6 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_7 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goParams___spec__1(x_1, x_5, x_6, x_4);
+lean_dec(x_1);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goParams___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Compiler_LCNF_LCtx_erase_goParams(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at_Lean_Compiler_LCNF_LCtx_erase___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -1491,6 +1706,46 @@ lean_dec(x_2);
 return x_3;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint8_t x_4; lean_object* x_5; 
+x_4 = lean_unbox(x_3);
+lean_dec(x_3);
+x_5 = l_Lean_Compiler_LCNF_LCtx_erase(x_1, x_2, x_4);
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goAlts___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+size_t x_5; size_t x_6; lean_object* x_7; 
+x_5 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_6 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_7 = l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_LCtx_erase_goAlts___spec__1(x_1, x_5, x_6, x_4);
+lean_dec(x_1);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_erase_goAlts___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Compiler_LCNF_LCtx_erase_goAlts(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LCtx_eraseFVarsAt(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Compiler_LCNF_LCtx_erase_go(x_1, x_2);
+return x_3;
+}
+}
 LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at_Lean_Compiler_LCNF_LCtx_toLocalContext___spec__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {

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

@@ -16,7 +16,6 @@ extern "C" {
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__13;
 lean_object* l_Lean_Compiler_LCNF_ppDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__23;
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__6;
 lean_object* l_Lean_KVMap_setBool(lean_object*, lean_object*, uint8_t);
 size_t lean_usize_add(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -28,8 +27,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_isMatcher___at_Lean_Compiler_LCNF_shouldGen
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isMatcher___at_Lean_Compiler_LCNF_shouldGenerateCode___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__2;
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__8;
 uint8_t lean_usize_dec_eq(size_t, size_t);
 lean_object* lean_array_uget(lean_object*, size_t);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -51,14 +48,15 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassMa
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__2;
 LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at_Lean_Compiler_LCNF_checkpoint___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__9;
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__2;
 uint8_t lean_usize_dec_lt(size_t, size_t);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__19;
 LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_Compiler_LCNF_PassManager_run___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__7;
 LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_Compiler_LCNF_checkpoint___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_PassInstaller_runFromDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___lambda__2___closed__1;
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__4;
 lean_object* l_Lean_Compiler_LCNF_saveStage1Decls(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__11;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -66,26 +64,28 @@ static lean_object* l_Lean_Compiler_LCNF_PassManager_run___lambda__1___closed__4
 extern lean_object* l_Lean_inheritedTraceOptions;
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__1;
 uint8_t l_Lean_Option_get___at_Lean_getSanitizeNames___spec__1(lean_object*, lean_object*);
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__8;
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__6;
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__3;
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__11;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__1;
 extern lean_object* l_Lean_Compiler_LCNF_PassInstaller_passInstallerExt;
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__4;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PassManager_run___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__3;
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__1;
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__7;
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__13;
 static lean_object* l_Lean_Compiler_LCNF_PassManager_run___lambda__1___closed__3;
 lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__12;
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__6;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___boxed(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_PassManager_run___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__1;
 lean_object* l_Std_mkHashMapImp___rarg(lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__4;
 LEAN_EXPORT lean_object* lean_compile_stage1(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__3;
 lean_object* l_Nat_repr(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__2;
@@ -98,12 +98,14 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint_
 lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__8;
 lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object*);
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__5;
 uint8_t l_Array_isEmpty___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isTypeFormerType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_ConstantInfo_type(lean_object*);
 lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Compiler_LCNF_checkDeadLocalDecls(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__7;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*, lean_object*);
@@ -125,15 +127,13 @@ uint8_t l___private_Lean_Util_Trace_0__Lean_checkTraceOption(lean_object*, lean_
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_PassManager_run___spec__4(lean_object*, size_t, size_t, 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_shouldGenerateCode___closed__20;
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__5;
 lean_object* l_Lean_Compiler_LCNF_CompilerM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__10;
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__7;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_run___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975_(lean_object*);
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_checkpoint___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__3;
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__5;
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__15;
@@ -143,7 +143,6 @@ LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at_Lean_Compiler_LCNF_chec
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__2___closed__5;
 lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_instBEqExpr;
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__9;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode_isCompIrrelevant(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__5;
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__14;
@@ -153,6 +152,7 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint_
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_PassManager_run___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isProp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_run___spec__3___closed__1;
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__9;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_PassManager_run___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_Decl_size(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_shouldGenerateCode___closed__22;
@@ -2015,6 +2015,9 @@ x_8 = lean_usize_of_nat(x_7);
 lean_dec(x_7);
 x_9 = 0;
 x_10 = lean_box(0);
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
 x_11 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3(x_1, x_2, x_8, x_9, x_10, x_3, x_4, x_5, x_6);
 if (lean_obj_tag(x_11) == 0)
 {
@@ -2022,44 +2025,87 @@ uint8_t x_12;
 x_12 = !lean_is_exclusive(x_11);
 if (x_12 == 0)
 {
-lean_object* x_13; 
-x_13 = lean_ctor_get(x_11, 0);
-lean_dec(x_13);
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; 
+x_13 = lean_ctor_get(x_11, 1);
+x_14 = lean_ctor_get(x_11, 0);
+lean_dec(x_14);
+x_15 = lean_ctor_get(x_4, 2);
+lean_inc(x_15);
+x_16 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__1___closed__1;
+x_17 = l_Lean_Option_get___at_Lean_getSanitizeNames___spec__1(x_15, x_16);
+lean_dec(x_15);
+if (x_17 == 0)
+{
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
 lean_ctor_set(x_11, 0, x_10);
 return x_11;
 }
 else
 {
-lean_object* x_14; lean_object* x_15; 
-x_14 = lean_ctor_get(x_11, 1);
-lean_inc(x_14);
-lean_dec(x_11);
-x_15 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_15, 0, x_10);
-lean_ctor_set(x_15, 1, x_14);
-return x_15;
+lean_object* x_18; 
+lean_free_object(x_11);
+x_18 = l_Lean_Compiler_LCNF_checkDeadLocalDecls(x_2, x_3, x_4, x_5, x_13);
+return x_18;
 }
 }
 else
 {
-uint8_t x_16; 
-x_16 = !lean_is_exclusive(x_11);
-if (x_16 == 0)
+lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; 
+x_19 = lean_ctor_get(x_11, 1);
+lean_inc(x_19);
+lean_dec(x_11);
+x_20 = lean_ctor_get(x_4, 2);
+lean_inc(x_20);
+x_21 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___lambda__1___closed__1;
+x_22 = l_Lean_Option_get___at_Lean_getSanitizeNames___spec__1(x_20, x_21);
+lean_dec(x_20);
+if (x_22 == 0)
+{
+lean_object* x_23; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_23 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_23, 0, x_10);
+lean_ctor_set(x_23, 1, x_19);
+return x_23;
+}
+else
+{
+lean_object* x_24; 
+x_24 = l_Lean_Compiler_LCNF_checkDeadLocalDecls(x_2, x_3, x_4, x_5, x_19);
+return x_24;
+}
+}
+}
+else
+{
+uint8_t x_25; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_25 = !lean_is_exclusive(x_11);
+if (x_25 == 0)
 {
 return x_11;
 }
 else
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-x_17 = lean_ctor_get(x_11, 0);
-x_18 = lean_ctor_get(x_11, 1);
-lean_inc(x_18);
-lean_inc(x_17);
+lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = lean_ctor_get(x_11, 0);
+x_27 = lean_ctor_get(x_11, 1);
+lean_inc(x_27);
+lean_inc(x_26);
 lean_dec(x_11);
-x_19 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_19, 0, x_17);
-lean_ctor_set(x_19, 1, x_18);
-return x_19;
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_26);
+lean_ctor_set(x_28, 1, x_27);
+return x_28;
 }
 }
 }
@@ -2118,15 +2164,6 @@ lean_dec(x_2);
 return x_12;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_checkpoint___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-lean_object* x_7; 
-x_7 = l_Lean_Compiler_LCNF_checkpoint(x_1, x_2, x_3, x_4, x_5, x_6);
-lean_dec(x_2);
-return x_7;
-}
-}
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_PassManager_run___spec__1(size_t x_1, size_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
@@ -2237,6 +2274,7 @@ lean_dec(x_9);
 x_12 = lean_ctor_get(x_1, 0);
 lean_inc(x_12);
 lean_dec(x_1);
+lean_inc(x_10);
 x_13 = l_Lean_Compiler_LCNF_checkpoint(x_12, x_10, x_4, x_5, x_6, x_11);
 if (lean_obj_tag(x_13) == 0)
 {
@@ -3189,7 +3227,7 @@ x_7 = l_Lean_Compiler_LCNF_CompilerM_run___rarg(x_5, x_6, x_2, x_3, x_4);
 return x_7;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__1() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -3199,7 +3237,7 @@ x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__2() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__2() {
 _start:
 {
 lean_object* x_1; 
@@ -3207,17 +3245,17 @@ x_1 = lean_mk_string_from_bytes("simp", 4);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__3() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__2;
-x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__2;
+x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__2;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__4() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__4() {
 _start:
 {
 lean_object* x_1; 
@@ -3225,17 +3263,17 @@ x_1 = lean_mk_string_from_bytes("pullInstances", 13);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__5() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__2;
-x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__4;
+x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__4;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__6() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__6() {
 _start:
 {
 lean_object* x_1; 
@@ -3243,17 +3281,17 @@ x_1 = lean_mk_string_from_bytes("cse", 3);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__7() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__2;
-x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__6;
+x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__6;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__8() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__8() {
 _start:
 {
 lean_object* x_1; 
@@ -3261,21 +3299,21 @@ x_1 = lean_mk_string_from_bytes("jp", 2);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__9() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_checkpoint___spec__3___closed__2;
-x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__8;
+x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__8;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__1;
+x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__1;
 x_3 = 1;
 x_4 = l_Lean_registerTraceClass(x_2, x_3, x_1);
 if (lean_obj_tag(x_4) == 0)
@@ -3284,7 +3322,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7;
 x_5 = lean_ctor_get(x_4, 1);
 lean_inc(x_5);
 lean_dec(x_4);
-x_6 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__3;
+x_6 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__3;
 x_7 = l_Lean_registerTraceClass(x_6, x_3, x_5);
 if (lean_obj_tag(x_7) == 0)
 {
@@ -3292,7 +3330,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10;
 x_8 = lean_ctor_get(x_7, 1);
 lean_inc(x_8);
 lean_dec(x_7);
-x_9 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__5;
+x_9 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__5;
 x_10 = l_Lean_registerTraceClass(x_9, x_3, x_8);
 if (lean_obj_tag(x_10) == 0)
 {
@@ -3300,7 +3338,7 @@ lean_object* x_11; lean_object* x_12; lean_object* x_13;
 x_11 = lean_ctor_get(x_10, 1);
 lean_inc(x_11);
 lean_dec(x_10);
-x_12 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__7;
+x_12 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__7;
 x_13 = l_Lean_registerTraceClass(x_12, x_3, x_11);
 if (lean_obj_tag(x_13) == 0)
 {
@@ -3308,7 +3346,7 @@ lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17;
 x_14 = lean_ctor_get(x_13, 1);
 lean_inc(x_14);
 lean_dec(x_13);
-x_15 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__9;
+x_15 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__9;
 x_16 = 0;
 x_17 = l_Lean_registerTraceClass(x_15, x_16, x_14);
 return x_17;
@@ -3557,25 +3595,25 @@ l_Lean_Compiler_LCNF_compileStage1Impl___closed__2 = _init_l_Lean_Compiler_LCNF_
 lean_mark_persistent(l_Lean_Compiler_LCNF_compileStage1Impl___closed__2);
 l_Lean_Compiler_LCNF_compileStage1Impl___closed__3 = _init_l_Lean_Compiler_LCNF_compileStage1Impl___closed__3();
 lean_mark_persistent(l_Lean_Compiler_LCNF_compileStage1Impl___closed__3);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__1();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__1);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__2 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__2();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__2);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__3 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__3();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__3);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__4 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__4();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__4);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__5 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__5();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__5);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__6 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__6();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__6);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__7 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__7();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__7);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__8 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__8();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__8);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__9 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__9();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948____closed__9);
-res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_948_(lean_io_mk_world());
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__1();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__1);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__2 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__2();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__2);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__3 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__3();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__3);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__4 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__4();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__4);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__5 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__5();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__5);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__6 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__6();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__6);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__7 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__7();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__7);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__8 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__8();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__8);
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__9 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__9();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975____closed__9);
+res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Main___hyg_975_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));

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

@@ -4200,7 +4200,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_Compiler_LCNF_PullLetDecls_pullDecls___lambda__1___closed__1;
 x_2 = l_Lean_Compiler_LCNF_PullLetDecls_pullDecls___lambda__1___closed__2;
-x_3 = lean_unsigned_to_nat(125u);
+x_3 = lean_unsigned_to_nat(181u);
 x_4 = lean_unsigned_to_nat(9u);
 x_5 = l_Lean_Compiler_LCNF_PullLetDecls_pullDecls___lambda__1___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -4920,7 +4920,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_Compiler_LCNF_PullLetDecls_pullDecls___lambda__1___closed__1;
 x_2 = l_Lean_Compiler_LCNF_PullLetDecls_pullDecls___lambda__2___closed__1;
-x_3 = lean_unsigned_to_nat(94u);
+x_3 = lean_unsigned_to_nat(150u);
 x_4 = lean_unsigned_to_nat(9u);
 x_5 = l_Lean_Compiler_LCNF_PullLetDecls_pullDecls___lambda__1___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@@ -112,6 +112,7 @@ lean_object* l_Lean_Meta_etaExpand(lean_object*, lean_object*, lean_object*, lea
 static lean_object* l_Lean_Compiler_LCNF_inlineMatchers___closed__20;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_macroInline(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l___private_Lean_Compiler_InlineAttrs_0__Lean_Compiler_hasInlineAttrAux(lean_object*, uint8_t, lean_object*);
+lean_object* l_Lean_Compiler_LCNF_eraseFVar(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_inlineMatchers___closed__10;
 static lean_object* l_Lean_Compiler_LCNF_inlineMatchers___closed__24;
@@ -2736,7 +2737,7 @@ return x_1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_toDecl(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_119; lean_object* x_120; lean_object* x_121; 
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_120; lean_object* x_121; lean_object* x_122; 
 x_6 = lean_st_ref_get(x_4, x_5);
 x_7 = lean_ctor_get(x_6, 0);
 lean_inc(x_7);
@@ -2746,42 +2747,42 @@ lean_dec(x_6);
 x_9 = lean_ctor_get(x_7, 0);
 lean_inc(x_9);
 lean_dec(x_7);
-x_119 = l_Lean_Compiler_LCNF_toDecl___closed__8;
+x_120 = l_Lean_Compiler_LCNF_toDecl___closed__8;
 lean_inc(x_1);
-x_120 = l_Lean_Name_str___override(x_1, x_119);
+x_121 = l_Lean_Name_str___override(x_1, x_120);
 lean_inc(x_9);
-x_121 = lean_environment_find(x_9, x_120);
-if (lean_obj_tag(x_121) == 0)
+x_122 = lean_environment_find(x_9, x_121);
+if (lean_obj_tag(x_122) == 0)
 {
-lean_object* x_122; 
+lean_object* x_123; 
 lean_inc(x_1);
-x_122 = lean_environment_find(x_9, x_1);
-x_10 = x_122;
-goto block_118;
+x_123 = lean_environment_find(x_9, x_1);
+x_10 = x_123;
+goto block_119;
 }
 else
 {
-uint8_t x_123; 
+uint8_t x_124; 
 lean_dec(x_9);
-x_123 = !lean_is_exclusive(x_121);
-if (x_123 == 0)
+x_124 = !lean_is_exclusive(x_122);
+if (x_124 == 0)
 {
-x_10 = x_121;
-goto block_118;
+x_10 = x_122;
+goto block_119;
 }
 else
 {
-lean_object* x_124; lean_object* x_125; 
-x_124 = lean_ctor_get(x_121, 0);
-lean_inc(x_124);
-lean_dec(x_121);
-x_125 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_125, 0, x_124);
-x_10 = x_125;
-goto block_118;
+lean_object* x_125; lean_object* x_126; 
+x_125 = lean_ctor_get(x_122, 0);
+lean_inc(x_125);
+lean_dec(x_122);
+x_126 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_126, 0, x_125);
+x_10 = x_126;
+goto block_119;
 }
 }
-block_118:
+block_119:
 {
 if (lean_obj_tag(x_10) == 0)
 {
@@ -2918,6 +2919,9 @@ lean_dec(x_31);
 x_56 = lean_ctor_get(x_55, 1);
 lean_inc(x_56);
 lean_dec(x_55);
+lean_inc(x_4);
+lean_inc(x_3);
+lean_inc(x_2);
 x_57 = l_Lean_Compiler_LCNF_ToLCNF_toLCNF(x_51, x_2, x_3, x_4, x_56);
 if (lean_obj_tag(x_57) == 0)
 {
@@ -2931,177 +2935,188 @@ x_59 = lean_ctor_get(x_58, 1);
 lean_inc(x_59);
 if (lean_obj_tag(x_59) == 5)
 {
-uint8_t x_60; 
+lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; uint8_t x_65; lean_object* x_66; uint8_t x_67; 
 lean_dec(x_59);
-x_60 = !lean_is_exclusive(x_57);
-if (x_60 == 0)
-{
-lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; 
-x_61 = lean_ctor_get(x_57, 0);
-lean_dec(x_61);
-x_62 = lean_ctor_get(x_58, 0);
-lean_inc(x_62);
+x_60 = lean_ctor_get(x_58, 0);
+lean_inc(x_60);
 lean_dec(x_58);
-x_63 = l_Lean_ConstantInfo_levelParams(x_17);
-lean_dec(x_17);
-x_64 = lean_ctor_get(x_62, 2);
-lean_inc(x_64);
-x_65 = lean_ctor_get(x_62, 4);
-lean_inc(x_65);
-lean_dec(x_62);
-x_66 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_66, 0, x_1);
-lean_ctor_set(x_66, 1, x_63);
-lean_ctor_set(x_66, 2, x_35);
-lean_ctor_set(x_66, 3, x_64);
-lean_ctor_set(x_66, 4, x_65);
-lean_ctor_set(x_57, 0, x_66);
-return x_57;
-}
-else
-{
-lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; 
-x_67 = lean_ctor_get(x_57, 1);
-lean_inc(x_67);
+x_61 = lean_ctor_get(x_57, 1);
+lean_inc(x_61);
 lean_dec(x_57);
-x_68 = lean_ctor_get(x_58, 0);
-lean_inc(x_68);
-lean_dec(x_58);
+x_62 = lean_ctor_get(x_60, 0);
+lean_inc(x_62);
+x_63 = lean_ctor_get(x_60, 2);
+lean_inc(x_63);
+x_64 = lean_ctor_get(x_60, 4);
+lean_inc(x_64);
+lean_dec(x_60);
+x_65 = 0;
+x_66 = l_Lean_Compiler_LCNF_eraseFVar(x_62, x_65, x_2, x_3, x_4, x_61);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_67 = !lean_is_exclusive(x_66);
+if (x_67 == 0)
+{
+lean_object* x_68; lean_object* x_69; lean_object* x_70; 
+x_68 = lean_ctor_get(x_66, 0);
+lean_dec(x_68);
 x_69 = l_Lean_ConstantInfo_levelParams(x_17);
 lean_dec(x_17);
-x_70 = lean_ctor_get(x_68, 2);
-lean_inc(x_70);
-x_71 = lean_ctor_get(x_68, 4);
+x_70 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_70, 0, x_1);
+lean_ctor_set(x_70, 1, x_69);
+lean_ctor_set(x_70, 2, x_35);
+lean_ctor_set(x_70, 3, x_63);
+lean_ctor_set(x_70, 4, x_64);
+lean_ctor_set(x_66, 0, x_70);
+return x_66;
+}
+else
+{
+lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; 
+x_71 = lean_ctor_get(x_66, 1);
 lean_inc(x_71);
-lean_dec(x_68);
-x_72 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_72, 0, x_1);
-lean_ctor_set(x_72, 1, x_69);
-lean_ctor_set(x_72, 2, x_35);
-lean_ctor_set(x_72, 3, x_70);
-lean_ctor_set(x_72, 4, x_71);
-x_73 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_73, 0, x_72);
-lean_ctor_set(x_73, 1, x_67);
-return x_73;
+lean_dec(x_66);
+x_72 = l_Lean_ConstantInfo_levelParams(x_17);
+lean_dec(x_17);
+x_73 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_73, 0, x_1);
+lean_ctor_set(x_73, 1, x_72);
+lean_ctor_set(x_73, 2, x_35);
+lean_ctor_set(x_73, 3, x_63);
+lean_ctor_set(x_73, 4, x_64);
+x_74 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_74, 0, x_73);
+lean_ctor_set(x_74, 1, x_71);
+return x_74;
 }
 }
 else
 {
-uint8_t x_74; 
+uint8_t x_75; 
 lean_dec(x_59);
-x_74 = !lean_is_exclusive(x_57);
-if (x_74 == 0)
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_75 = !lean_is_exclusive(x_57);
+if (x_75 == 0)
 {
-lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; 
-x_75 = lean_ctor_get(x_57, 0);
-lean_dec(x_75);
-x_76 = l_Lean_ConstantInfo_levelParams(x_17);
+lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; 
+x_76 = lean_ctor_get(x_57, 0);
+lean_dec(x_76);
+x_77 = l_Lean_ConstantInfo_levelParams(x_17);
 lean_dec(x_17);
-x_77 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
-x_78 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_78, 0, x_1);
-lean_ctor_set(x_78, 1, x_76);
-lean_ctor_set(x_78, 2, x_35);
-lean_ctor_set(x_78, 3, x_77);
-lean_ctor_set(x_78, 4, x_58);
-lean_ctor_set(x_57, 0, x_78);
+x_78 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
+x_79 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_79, 0, x_1);
+lean_ctor_set(x_79, 1, x_77);
+lean_ctor_set(x_79, 2, x_35);
+lean_ctor_set(x_79, 3, x_78);
+lean_ctor_set(x_79, 4, x_58);
+lean_ctor_set(x_57, 0, x_79);
 return x_57;
 }
 else
 {
-lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; 
-x_79 = lean_ctor_get(x_57, 1);
-lean_inc(x_79);
+lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; 
+x_80 = lean_ctor_get(x_57, 1);
+lean_inc(x_80);
 lean_dec(x_57);
-x_80 = l_Lean_ConstantInfo_levelParams(x_17);
+x_81 = l_Lean_ConstantInfo_levelParams(x_17);
 lean_dec(x_17);
-x_81 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
-x_82 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_82, 0, x_1);
-lean_ctor_set(x_82, 1, x_80);
-lean_ctor_set(x_82, 2, x_35);
-lean_ctor_set(x_82, 3, x_81);
-lean_ctor_set(x_82, 4, x_58);
-x_83 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_83, 0, x_82);
-lean_ctor_set(x_83, 1, x_79);
-return x_83;
+x_82 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
+x_83 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_83, 0, x_1);
+lean_ctor_set(x_83, 1, x_81);
+lean_ctor_set(x_83, 2, x_35);
+lean_ctor_set(x_83, 3, x_82);
+lean_ctor_set(x_83, 4, x_58);
+x_84 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_84, 0, x_83);
+lean_ctor_set(x_84, 1, x_80);
+return x_84;
 }
 }
 }
 else
 {
-uint8_t x_84; 
-x_84 = !lean_is_exclusive(x_57);
-if (x_84 == 0)
+uint8_t x_85; 
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_85 = !lean_is_exclusive(x_57);
+if (x_85 == 0)
 {
-lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; 
-x_85 = lean_ctor_get(x_57, 0);
-lean_dec(x_85);
-x_86 = l_Lean_ConstantInfo_levelParams(x_17);
+lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; 
+x_86 = lean_ctor_get(x_57, 0);
+lean_dec(x_86);
+x_87 = l_Lean_ConstantInfo_levelParams(x_17);
 lean_dec(x_17);
-x_87 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
-x_88 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_88, 0, x_1);
-lean_ctor_set(x_88, 1, x_86);
-lean_ctor_set(x_88, 2, x_35);
-lean_ctor_set(x_88, 3, x_87);
-lean_ctor_set(x_88, 4, x_58);
-lean_ctor_set(x_57, 0, x_88);
+x_88 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
+x_89 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_89, 0, x_1);
+lean_ctor_set(x_89, 1, x_87);
+lean_ctor_set(x_89, 2, x_35);
+lean_ctor_set(x_89, 3, x_88);
+lean_ctor_set(x_89, 4, x_58);
+lean_ctor_set(x_57, 0, x_89);
 return x_57;
 }
 else
 {
-lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; 
-x_89 = lean_ctor_get(x_57, 1);
-lean_inc(x_89);
+lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; 
+x_90 = lean_ctor_get(x_57, 1);
+lean_inc(x_90);
 lean_dec(x_57);
-x_90 = l_Lean_ConstantInfo_levelParams(x_17);
+x_91 = l_Lean_ConstantInfo_levelParams(x_17);
 lean_dec(x_17);
-x_91 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
-x_92 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_92, 0, x_1);
-lean_ctor_set(x_92, 1, x_90);
-lean_ctor_set(x_92, 2, x_35);
-lean_ctor_set(x_92, 3, x_91);
-lean_ctor_set(x_92, 4, x_58);
-x_93 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_93, 0, x_92);
-lean_ctor_set(x_93, 1, x_89);
-return x_93;
+x_92 = l_Lean_Compiler_LCNF_inlineMatchers___lambda__2___closed__1;
+x_93 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_93, 0, x_1);
+lean_ctor_set(x_93, 1, x_91);
+lean_ctor_set(x_93, 2, x_35);
+lean_ctor_set(x_93, 3, x_92);
+lean_ctor_set(x_93, 4, x_58);
+x_94 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_94, 0, x_93);
+lean_ctor_set(x_94, 1, x_90);
+return x_94;
 }
 }
 }
 else
 {
-uint8_t x_94; 
+uint8_t x_95; 
 lean_dec(x_35);
 lean_dec(x_17);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
 lean_dec(x_1);
-x_94 = !lean_is_exclusive(x_57);
-if (x_94 == 0)
+x_95 = !lean_is_exclusive(x_57);
+if (x_95 == 0)
 {
 return x_57;
 }
 else
 {
-lean_object* x_95; lean_object* x_96; lean_object* x_97; 
-x_95 = lean_ctor_get(x_57, 0);
-x_96 = lean_ctor_get(x_57, 1);
+lean_object* x_96; lean_object* x_97; lean_object* x_98; 
+x_96 = lean_ctor_get(x_57, 0);
+x_97 = lean_ctor_get(x_57, 1);
+lean_inc(x_97);
 lean_inc(x_96);
-lean_inc(x_95);
 lean_dec(x_57);
-x_97 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_97, 0, x_95);
-lean_ctor_set(x_97, 1, x_96);
-return x_97;
+x_98 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_98, 0, x_96);
+lean_ctor_set(x_98, 1, x_97);
+return x_98;
 }
 }
 }
 else
 {
-uint8_t x_98; 
+uint8_t x_99; 
 lean_dec(x_35);
 lean_dec(x_31);
 lean_dec(x_17);
@@ -3109,29 +3124,29 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_98 = !lean_is_exclusive(x_50);
-if (x_98 == 0)
+x_99 = !lean_is_exclusive(x_50);
+if (x_99 == 0)
 {
 return x_50;
 }
 else
 {
-lean_object* x_99; lean_object* x_100; lean_object* x_101; 
-x_99 = lean_ctor_get(x_50, 0);
-x_100 = lean_ctor_get(x_50, 1);
+lean_object* x_100; lean_object* x_101; lean_object* x_102; 
+x_100 = lean_ctor_get(x_50, 0);
+x_101 = lean_ctor_get(x_50, 1);
+lean_inc(x_101);
 lean_inc(x_100);
-lean_inc(x_99);
 lean_dec(x_50);
-x_101 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_101, 0, x_99);
-lean_ctor_set(x_101, 1, x_100);
-return x_101;
+x_102 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_102, 0, x_100);
+lean_ctor_set(x_102, 1, x_101);
+return x_102;
 }
 }
 }
 else
 {
-uint8_t x_102; 
+uint8_t x_103; 
 lean_dec(x_35);
 lean_dec(x_31);
 lean_dec(x_17);
@@ -3139,29 +3154,29 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_102 = !lean_is_exclusive(x_47);
-if (x_102 == 0)
+x_103 = !lean_is_exclusive(x_47);
+if (x_103 == 0)
 {
 return x_47;
 }
 else
 {
-lean_object* x_103; lean_object* x_104; lean_object* x_105; 
-x_103 = lean_ctor_get(x_47, 0);
-x_104 = lean_ctor_get(x_47, 1);
+lean_object* x_104; lean_object* x_105; lean_object* x_106; 
+x_104 = lean_ctor_get(x_47, 0);
+x_105 = lean_ctor_get(x_47, 1);
+lean_inc(x_105);
 lean_inc(x_104);
-lean_inc(x_103);
 lean_dec(x_47);
-x_105 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_105, 0, x_103);
-lean_ctor_set(x_105, 1, x_104);
-return x_105;
+x_106 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_106, 0, x_104);
+lean_ctor_set(x_106, 1, x_105);
+return x_106;
 }
 }
 }
 else
 {
-uint8_t x_106; 
+uint8_t x_107; 
 lean_dec(x_35);
 lean_dec(x_31);
 lean_dec(x_17);
@@ -3169,29 +3184,29 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_106 = !lean_is_exclusive(x_43);
-if (x_106 == 0)
+x_107 = !lean_is_exclusive(x_43);
+if (x_107 == 0)
 {
 return x_43;
 }
 else
 {
-lean_object* x_107; lean_object* x_108; lean_object* x_109; 
-x_107 = lean_ctor_get(x_43, 0);
-x_108 = lean_ctor_get(x_43, 1);
+lean_object* x_108; lean_object* x_109; lean_object* x_110; 
+x_108 = lean_ctor_get(x_43, 0);
+x_109 = lean_ctor_get(x_43, 1);
+lean_inc(x_109);
 lean_inc(x_108);
-lean_inc(x_107);
 lean_dec(x_43);
-x_109 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_109, 0, x_107);
-lean_ctor_set(x_109, 1, x_108);
-return x_109;
+x_110 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_110, 0, x_108);
+lean_ctor_set(x_110, 1, x_109);
+return x_110;
 }
 }
 }
 else
 {
-uint8_t x_110; 
+uint8_t x_111; 
 lean_dec(x_35);
 lean_dec(x_31);
 lean_dec(x_17);
@@ -3199,29 +3214,29 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_110 = !lean_is_exclusive(x_38);
-if (x_110 == 0)
+x_111 = !lean_is_exclusive(x_38);
+if (x_111 == 0)
 {
 return x_38;
 }
 else
 {
-lean_object* x_111; lean_object* x_112; lean_object* x_113; 
-x_111 = lean_ctor_get(x_38, 0);
-x_112 = lean_ctor_get(x_38, 1);
+lean_object* x_112; lean_object* x_113; lean_object* x_114; 
+x_112 = lean_ctor_get(x_38, 0);
+x_113 = lean_ctor_get(x_38, 1);
+lean_inc(x_113);
 lean_inc(x_112);
-lean_inc(x_111);
 lean_dec(x_38);
-x_113 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_113, 0, x_111);
-lean_ctor_set(x_113, 1, x_112);
-return x_113;
+x_114 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_114, 0, x_112);
+lean_ctor_set(x_114, 1, x_113);
+return x_114;
 }
 }
 }
 else
 {
-uint8_t x_114; 
+uint8_t x_115; 
 lean_dec(x_31);
 lean_dec(x_25);
 lean_dec(x_17);
@@ -3229,23 +3244,23 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_114 = !lean_is_exclusive(x_34);
-if (x_114 == 0)
+x_115 = !lean_is_exclusive(x_34);
+if (x_115 == 0)
 {
 return x_34;
 }
 else
 {
-lean_object* x_115; lean_object* x_116; lean_object* x_117; 
-x_115 = lean_ctor_get(x_34, 0);
-x_116 = lean_ctor_get(x_34, 1);
+lean_object* x_116; lean_object* x_117; lean_object* x_118; 
+x_116 = lean_ctor_get(x_34, 0);
+x_117 = lean_ctor_get(x_34, 1);
+lean_inc(x_117);
 lean_inc(x_116);
-lean_inc(x_115);
 lean_dec(x_34);
-x_117 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_117, 0, x_115);
-lean_ctor_set(x_117, 1, x_116);
-return x_117;
+x_118 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_118, 0, x_116);
+lean_ctor_set(x_118, 1, x_117);
+return x_118;
 }
 }
 }

stage0/stdlib/Lean/Server/AsyncList.c

@@ -23,16 +23,16 @@ LEAN_EXPORT lean_object* l_IO_AsyncList_waitHead_x3f(lean_object*, lean_object*)
 LEAN_EXPORT lean_object* l_IO_AsyncList_instInhabitedAsyncList(lean_object*, lean_object*);
 static lean_object* l_IO_AsyncList_waitFind_x3f___rarg___closed__2;
 LEAN_EXPORT lean_object* l_IO_AsyncList_unfoldAsync(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitHead_x3f___rarg(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitHead_x3f___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg___lambda__1(lean_object*, lean_object*);
 static lean_object* l_IO_AsyncList_instAppendAsyncList___closed__1;
 static lean_object* l_IO_AsyncList_instCoeListAsyncList___closed__1;
 lean_object* l_Except_map___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg___lambda__2(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_append___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_foldr___at_IO_AsyncList_ofList___spec__1(lean_object*, lean_object*);
 lean_object* lean_io_as_task(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg(lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_IO_AsyncList_waitHead_x3f___rarg___lambda__1(lean_object*);
 lean_object* lean_task_map(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_instCoeListAsyncList(lean_object*, lean_object*);
@@ -43,20 +43,20 @@ extern lean_object* l_Task_Priority_default;
 lean_object* lean_io_has_finished(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_ofList___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_unfoldAsync_step(lean_object*, lean_object*, lean_object*);
-lean_object* lean_io_bind_task(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_append(lean_object*, lean_object*);
+lean_object* lean_task_bind(lean_object*, lean_object*, lean_object*);
 static lean_object* l_IO_AsyncList_waitHead_x3f___rarg___closed__1;
 LEAN_EXPORT lean_object* l_IO_AsyncList_getAll(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_unfoldAsync_step___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_instAppendAsyncList(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_ofList(lean_object*, lean_object*);
 lean_object* l_EIO_toBaseIO___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_unfoldAsync___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_task_pure(lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_getFinishedPrefix___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* lean_task_get_own(lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_waitHead_x3f___rarg___lambda__1___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_IO_AsyncList_instInhabitedAsyncList(lean_object* x_1, lean_object* x_2) {
@@ -577,36 +577,33 @@ return x_9;
 }
 }
 }
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg___lambda__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 if (lean_obj_tag(x_2) == 0)
 {
-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_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 lean_dec(x_1);
-x_4 = lean_ctor_get(x_2, 0);
-lean_inc(x_4);
+x_3 = lean_ctor_get(x_2, 0);
+lean_inc(x_3);
 lean_dec(x_2);
-x_5 = lean_box(0);
-x_6 = lean_alloc_ctor(1, 1, 0);
+x_4 = lean_box(0);
+x_5 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_5, 0, x_3);
+x_6 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_6, 0, x_4);
-x_7 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_7, 0, x_5);
-lean_ctor_set(x_7, 1, x_6);
-x_8 = lean_task_pure(x_7);
-x_9 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_9, 0, x_8);
-lean_ctor_set(x_9, 1, x_3);
-return x_9;
+lean_ctor_set(x_6, 1, x_5);
+x_7 = lean_task_pure(x_6);
+return x_7;
 }
 else
 {
-lean_object* x_10; lean_object* x_11; 
-x_10 = lean_ctor_get(x_2, 0);
-lean_inc(x_10);
+lean_object* x_8; lean_object* x_9; 
+x_8 = lean_ctor_get(x_2, 0);
+lean_inc(x_8);
 lean_dec(x_2);
-x_11 = l_IO_AsyncList_waitAll___rarg(x_1, x_10, x_3);
-return x_11;
+x_9 = l_IO_AsyncList_waitAll___rarg(x_1, x_8);
+return x_9;
 }
 }
 }
@@ -619,125 +616,68 @@ x_2 = lean_task_pure(x_1);
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 switch (lean_obj_tag(x_2)) {
 case 0:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; 
-x_4 = lean_ctor_get(x_2, 0);
+lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; 
+x_3 = lean_ctor_get(x_2, 0);
+lean_inc(x_3);
+x_4 = lean_ctor_get(x_2, 1);
 lean_inc(x_4);
-x_5 = lean_ctor_get(x_2, 1);
-lean_inc(x_5);
 lean_dec(x_2);
 lean_inc(x_1);
-lean_inc(x_4);
-x_6 = lean_apply_1(x_1, x_4);
-x_7 = lean_unbox(x_6);
-lean_dec(x_6);
-if (x_7 == 0)
-{
-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_inc(x_3);
+x_5 = lean_apply_1(x_1, x_3);
+x_6 = lean_unbox(x_5);
 lean_dec(x_5);
-lean_dec(x_1);
-x_8 = lean_box(0);
-x_9 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_9, 0, x_4);
-lean_ctor_set(x_9, 1, x_8);
-x_10 = lean_box(0);
-x_11 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_11, 0, x_9);
-lean_ctor_set(x_11, 1, x_10);
-x_12 = lean_task_pure(x_11);
-x_13 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_13, 0, x_12);
-lean_ctor_set(x_13, 1, x_3);
-return x_13;
-}
-else
+if (x_6 == 0)
 {
-lean_object* x_14; 
-x_14 = l_IO_AsyncList_waitAll___rarg(x_1, x_5, x_3);
-if (lean_obj_tag(x_14) == 0)
-{
-uint8_t x_15; 
-x_15 = !lean_is_exclusive(x_14);
-if (x_15 == 0)
-{
-lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-x_16 = lean_ctor_get(x_14, 0);
-x_17 = lean_alloc_closure((void*)(l_IO_AsyncList_waitAll___rarg___lambda__1), 2, 1);
-lean_closure_set(x_17, 0, x_4);
-x_18 = l_Task_Priority_default;
-x_19 = lean_task_map(x_17, x_16, x_18);
-lean_ctor_set(x_14, 0, x_19);
-return x_14;
-}
-else
-{
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; 
-x_20 = lean_ctor_get(x_14, 0);
-x_21 = lean_ctor_get(x_14, 1);
-lean_inc(x_21);
-lean_inc(x_20);
-lean_dec(x_14);
-x_22 = lean_alloc_closure((void*)(l_IO_AsyncList_waitAll___rarg___lambda__1), 2, 1);
-lean_closure_set(x_22, 0, x_4);
-x_23 = l_Task_Priority_default;
-x_24 = lean_task_map(x_22, x_20, x_23);
-x_25 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_25, 0, x_24);
-lean_ctor_set(x_25, 1, x_21);
-return x_25;
-}
-}
-else
-{
-uint8_t x_26; 
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
 lean_dec(x_4);
-x_26 = !lean_is_exclusive(x_14);
-if (x_26 == 0)
-{
-return x_14;
+lean_dec(x_1);
+x_7 = lean_box(0);
+x_8 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_8, 0, x_3);
+lean_ctor_set(x_8, 1, x_7);
+x_9 = lean_box(0);
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_8);
+lean_ctor_set(x_10, 1, x_9);
+x_11 = lean_task_pure(x_10);
+return x_11;
 }
 else
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; 
-x_27 = lean_ctor_get(x_14, 0);
-x_28 = lean_ctor_get(x_14, 1);
-lean_inc(x_28);
-lean_inc(x_27);
-lean_dec(x_14);
-x_29 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_29, 0, x_27);
-lean_ctor_set(x_29, 1, x_28);
-return x_29;
-}
-}
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_12 = lean_alloc_closure((void*)(l_IO_AsyncList_waitAll___rarg___lambda__1), 2, 1);
+lean_closure_set(x_12, 0, x_3);
+x_13 = l_IO_AsyncList_waitAll___rarg(x_1, x_4);
+x_14 = l_Task_Priority_default;
+x_15 = lean_task_map(x_12, x_13, x_14);
+return x_15;
 }
 }
 case 1:
 {
-lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_30 = lean_ctor_get(x_2, 0);
-lean_inc(x_30);
+lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_16 = lean_ctor_get(x_2, 0);
+lean_inc(x_16);
 lean_dec(x_2);
-x_31 = lean_alloc_closure((void*)(l_IO_AsyncList_waitAll___rarg___lambda__2), 3, 1);
-lean_closure_set(x_31, 0, x_1);
-x_32 = l_Task_Priority_default;
-x_33 = lean_io_bind_task(x_30, x_31, x_32, x_3);
-return x_33;
+x_17 = lean_alloc_closure((void*)(l_IO_AsyncList_waitAll___rarg___lambda__2), 2, 1);
+lean_closure_set(x_17, 0, x_1);
+x_18 = l_Task_Priority_default;
+x_19 = lean_task_bind(x_16, x_17, x_18);
+return x_19;
 }
 default: 
 {
-lean_object* x_34; lean_object* x_35; 
+lean_object* x_20; 
 lean_dec(x_1);
-x_34 = l_IO_AsyncList_waitAll___rarg___closed__1;
-x_35 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_35, 0, x_34);
-lean_ctor_set(x_35, 1, x_3);
-return x_35;
+x_20 = l_IO_AsyncList_waitAll___rarg___closed__1;
+return x_20;
 }
 }
 }
@@ -746,50 +686,44 @@ LEAN_EXPORT lean_object* l_IO_AsyncList_waitAll(lean_object* x_1, lean_object* x
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_IO_AsyncList_waitAll___rarg), 3, 0);
+x_3 = lean_alloc_closure((void*)(l_IO_AsyncList_waitAll___rarg), 2, 0);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 if (lean_obj_tag(x_2) == 0)
 {
-uint8_t x_4; 
+uint8_t x_3; 
 lean_dec(x_1);
-x_4 = !lean_is_exclusive(x_2);
-if (x_4 == 0)
+x_3 = !lean_is_exclusive(x_2);
+if (x_3 == 0)
 {
-lean_object* x_5; lean_object* x_6; 
-x_5 = lean_task_pure(x_2);
-x_6 = lean_alloc_ctor(0, 2, 0);
+lean_object* x_4; 
+x_4 = lean_task_pure(x_2);
+return x_4;
+}
+else
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_5 = lean_ctor_get(x_2, 0);
+lean_inc(x_5);
+lean_dec(x_2);
+x_6 = lean_alloc_ctor(0, 1, 0);
 lean_ctor_set(x_6, 0, x_5);
-lean_ctor_set(x_6, 1, x_3);
-return x_6;
-}
-else
-{
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_7 = lean_ctor_get(x_2, 0);
-lean_inc(x_7);
-lean_dec(x_2);
-x_8 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_8, 0, x_7);
-x_9 = lean_task_pure(x_8);
-x_10 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_10, 0, x_9);
-lean_ctor_set(x_10, 1, x_3);
-return x_10;
+x_7 = lean_task_pure(x_6);
+return x_7;
 }
 }
 else
 {
-lean_object* x_11; lean_object* x_12; 
-x_11 = lean_ctor_get(x_2, 0);
-lean_inc(x_11);
+lean_object* x_8; lean_object* x_9; 
+x_8 = lean_ctor_get(x_2, 0);
+lean_inc(x_8);
 lean_dec(x_2);
-x_12 = l_IO_AsyncList_waitFind_x3f___rarg(x_1, x_11, x_3);
-return x_12;
+x_9 = l_IO_AsyncList_waitFind_x3f___rarg(x_1, x_8);
+return x_9;
 }
 }
 }
@@ -812,66 +746,60 @@ x_2 = lean_task_pure(x_1);
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 switch (lean_obj_tag(x_2)) {
 case 0:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; 
-x_4 = lean_ctor_get(x_2, 0);
+lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; 
+x_3 = lean_ctor_get(x_2, 0);
+lean_inc(x_3);
+x_4 = lean_ctor_get(x_2, 1);
 lean_inc(x_4);
-x_5 = lean_ctor_get(x_2, 1);
-lean_inc(x_5);
 lean_dec(x_2);
 lean_inc(x_1);
-lean_inc(x_4);
-x_6 = lean_apply_1(x_1, x_4);
-x_7 = lean_unbox(x_6);
-lean_dec(x_6);
-if (x_7 == 0)
+lean_inc(x_3);
+x_5 = lean_apply_1(x_1, x_3);
+x_6 = lean_unbox(x_5);
+lean_dec(x_5);
+if (x_6 == 0)
 {
-lean_dec(x_4);
-x_2 = x_5;
+lean_dec(x_3);
+x_2 = x_4;
 goto _start;
 }
 else
 {
-lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-lean_dec(x_5);
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+lean_dec(x_4);
 lean_dec(x_1);
+x_8 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_8, 0, x_3);
 x_9 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_9, 0, x_4);
-x_10 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_10, 0, x_9);
-x_11 = lean_task_pure(x_10);
-x_12 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_12, 0, x_11);
-lean_ctor_set(x_12, 1, x_3);
-return x_12;
+lean_ctor_set(x_9, 0, x_8);
+x_10 = lean_task_pure(x_9);
+return x_10;
 }
 }
 case 1:
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_13 = lean_ctor_get(x_2, 0);
-lean_inc(x_13);
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_11 = lean_ctor_get(x_2, 0);
+lean_inc(x_11);
 lean_dec(x_2);
-x_14 = lean_alloc_closure((void*)(l_IO_AsyncList_waitFind_x3f___rarg___lambda__1), 3, 1);
-lean_closure_set(x_14, 0, x_1);
-x_15 = l_Task_Priority_default;
-x_16 = lean_io_bind_task(x_13, x_14, x_15, x_3);
-return x_16;
+x_12 = lean_alloc_closure((void*)(l_IO_AsyncList_waitFind_x3f___rarg___lambda__1), 2, 1);
+lean_closure_set(x_12, 0, x_1);
+x_13 = l_Task_Priority_default;
+x_14 = lean_task_bind(x_11, x_12, x_13);
+return x_14;
 }
 default: 
 {
-lean_object* x_17; lean_object* x_18; 
+lean_object* x_15; 
 lean_dec(x_1);
-x_17 = l_IO_AsyncList_waitFind_x3f___rarg___closed__2;
-x_18 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_18, 0, x_17);
-lean_ctor_set(x_18, 1, x_3);
-return x_18;
+x_15 = l_IO_AsyncList_waitFind_x3f___rarg___closed__2;
+return x_15;
 }
 }
 }
@@ -880,7 +808,7 @@ LEAN_EXPORT lean_object* l_IO_AsyncList_waitFind_x3f(lean_object* x_1, lean_obje
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_IO_AsyncList_waitFind_x3f___rarg), 3, 0);
+x_3 = lean_alloc_closure((void*)(l_IO_AsyncList_waitFind_x3f___rarg), 2, 0);
 return x_3;
 }
 }
@@ -1170,20 +1098,20 @@ x_1 = lean_alloc_closure((void*)(l_IO_AsyncList_waitHead_x3f___rarg___lambda__1_
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_IO_AsyncList_waitHead_x3f___rarg(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_IO_AsyncList_waitHead_x3f___rarg(lean_object* x_1) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; 
-x_3 = l_IO_AsyncList_waitHead_x3f___rarg___closed__1;
-x_4 = l_IO_AsyncList_waitFind_x3f___rarg(x_3, x_1, x_2);
-return x_4;
+lean_object* x_2; lean_object* x_3; 
+x_2 = l_IO_AsyncList_waitHead_x3f___rarg___closed__1;
+x_3 = l_IO_AsyncList_waitFind_x3f___rarg(x_2, x_1);
+return x_3;
 }
 }
 LEAN_EXPORT lean_object* l_IO_AsyncList_waitHead_x3f(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_IO_AsyncList_waitHead_x3f___rarg), 2, 0);
+x_3 = lean_alloc_closure((void*)(l_IO_AsyncList_waitHead_x3f___rarg), 1, 0);
 return x_3;
 }
 }

stage0/stdlib/Lean/Server/FileWorker.c

@@ -396,7 +396,7 @@ lean_object* l_Lean_Server_Snapshots_Snapshot_endPos(lean_object*);
 static lean_object* l_IO_FS_Stream_readRequestAs___at_Lean_Server_FileWorker_initAndRunWorker___spec__2___closed__25;
 LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_compileHeader___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_Server_FileWorker_queueRequest___spec__2(lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object*, lean_object*);
 lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_RBNode_erase___at_Lean_Server_FileWorker_mainLoop___spec__2(uint64_t, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -7380,7 +7380,7 @@ lean_inc(x_9);
 x_10 = l_Lean_Parser_parseHeader(x_9, x_7);
 if (lean_obj_tag(x_10) == 0)
 {
-lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; 
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32; 
 x_11 = lean_ctor_get(x_10, 0);
 lean_inc(x_11);
 x_12 = lean_ctor_get(x_11, 1);
@@ -7404,131 +7404,126 @@ x_19 = lean_ctor_get(x_8, 1);
 lean_inc(x_19);
 x_20 = l_Lean_Server_FileWorker_updateDocument___closed__1;
 lean_inc(x_19);
-x_21 = l_IO_AsyncList_waitFind_x3f___rarg(x_20, x_19, x_18);
-x_22 = lean_ctor_get(x_21, 0);
-lean_inc(x_22);
-x_23 = lean_ctor_get(x_21, 1);
-lean_inc(x_23);
-lean_dec(x_21);
+x_21 = l_IO_AsyncList_waitFind_x3f___rarg(x_20, x_19);
 lean_inc(x_17);
 lean_inc(x_1);
-x_24 = lean_alloc_closure((void*)(l_Lean_Server_FileWorker_updateDocument___lambda__3___boxed), 10, 8);
-lean_closure_set(x_24, 0, x_8);
-lean_closure_set(x_24, 1, x_14);
-lean_closure_set(x_24, 2, x_15);
-lean_closure_set(x_24, 3, x_1);
-lean_closure_set(x_24, 4, x_19);
-lean_closure_set(x_24, 5, x_17);
-lean_closure_set(x_24, 6, x_2);
-lean_closure_set(x_24, 7, x_9);
-x_25 = l_Task_Priority_default;
-x_26 = lean_io_map_task(x_24, x_22, x_25, x_23);
-x_27 = lean_ctor_get(x_26, 0);
-lean_inc(x_27);
-x_28 = lean_ctor_get(x_26, 1);
+x_22 = lean_alloc_closure((void*)(l_Lean_Server_FileWorker_updateDocument___lambda__3___boxed), 10, 8);
+lean_closure_set(x_22, 0, x_8);
+lean_closure_set(x_22, 1, x_14);
+lean_closure_set(x_22, 2, x_15);
+lean_closure_set(x_22, 3, x_1);
+lean_closure_set(x_22, 4, x_19);
+lean_closure_set(x_22, 5, x_17);
+lean_closure_set(x_22, 6, x_2);
+lean_closure_set(x_22, 7, x_9);
+x_23 = l_Task_Priority_default;
+x_24 = lean_io_map_task(x_22, x_21, x_23, x_18);
+x_25 = lean_ctor_get(x_24, 0);
+lean_inc(x_25);
+x_26 = lean_ctor_get(x_24, 1);
+lean_inc(x_26);
+lean_dec(x_24);
+x_27 = lean_st_ref_take(x_3, x_26);
+x_28 = lean_ctor_get(x_27, 0);
 lean_inc(x_28);
-lean_dec(x_26);
-x_29 = lean_st_ref_take(x_3, x_28);
-x_30 = lean_ctor_get(x_29, 0);
-lean_inc(x_30);
-x_31 = lean_ctor_get(x_29, 1);
-lean_inc(x_31);
-lean_dec(x_29);
-x_32 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_32, 0, x_27);
-x_33 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_33, 0, x_1);
-lean_ctor_set(x_33, 1, x_32);
-lean_ctor_set(x_33, 2, x_17);
-x_34 = !lean_is_exclusive(x_30);
-if (x_34 == 0)
+x_29 = lean_ctor_get(x_27, 1);
+lean_inc(x_29);
+lean_dec(x_27);
+x_30 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_30, 0, x_25);
+x_31 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_31, 0, x_1);
+lean_ctor_set(x_31, 1, x_30);
+lean_ctor_set(x_31, 2, x_17);
+x_32 = !lean_is_exclusive(x_28);
+if (x_32 == 0)
 {
-lean_object* x_35; lean_object* x_36; uint8_t x_37; 
-x_35 = lean_ctor_get(x_30, 0);
-lean_dec(x_35);
-lean_ctor_set(x_30, 0, x_33);
-x_36 = lean_st_ref_set(x_3, x_30, x_31);
-x_37 = !lean_is_exclusive(x_36);
-if (x_37 == 0)
+lean_object* x_33; lean_object* x_34; uint8_t x_35; 
+x_33 = lean_ctor_get(x_28, 0);
+lean_dec(x_33);
+lean_ctor_set(x_28, 0, x_31);
+x_34 = lean_st_ref_set(x_3, x_28, x_29);
+x_35 = !lean_is_exclusive(x_34);
+if (x_35 == 0)
 {
-lean_object* x_38; lean_object* x_39; 
-x_38 = lean_ctor_get(x_36, 0);
-lean_dec(x_38);
-x_39 = lean_box(0);
-lean_ctor_set(x_36, 0, x_39);
-return x_36;
-}
-else
-{
-lean_object* x_40; lean_object* x_41; lean_object* x_42; 
-x_40 = lean_ctor_get(x_36, 1);
-lean_inc(x_40);
+lean_object* x_36; lean_object* x_37; 
+x_36 = lean_ctor_get(x_34, 0);
 lean_dec(x_36);
-x_41 = lean_box(0);
-x_42 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_42, 0, x_41);
-lean_ctor_set(x_42, 1, x_40);
-return x_42;
+x_37 = lean_box(0);
+lean_ctor_set(x_34, 0, x_37);
+return x_34;
+}
+else
+{
+lean_object* x_38; lean_object* x_39; lean_object* x_40; 
+x_38 = lean_ctor_get(x_34, 1);
+lean_inc(x_38);
+lean_dec(x_34);
+x_39 = lean_box(0);
+x_40 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_40, 0, x_39);
+lean_ctor_set(x_40, 1, x_38);
+return x_40;
 }
 }
 else
 {
-lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; 
-x_43 = lean_ctor_get(x_30, 1);
-x_44 = lean_ctor_get(x_30, 2);
-lean_inc(x_44);
-lean_inc(x_43);
-lean_dec(x_30);
-x_45 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_45, 0, x_33);
-lean_ctor_set(x_45, 1, x_43);
-lean_ctor_set(x_45, 2, x_44);
-x_46 = lean_st_ref_set(x_3, x_45, x_31);
-x_47 = lean_ctor_get(x_46, 1);
-lean_inc(x_47);
-if (lean_is_exclusive(x_46)) {
- lean_ctor_release(x_46, 0);
- lean_ctor_release(x_46, 1);
+lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; 
+x_41 = lean_ctor_get(x_28, 1);
+x_42 = lean_ctor_get(x_28, 2);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_dec(x_28);
+x_43 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_43, 0, x_31);
+lean_ctor_set(x_43, 1, x_41);
+lean_ctor_set(x_43, 2, x_42);
+x_44 = lean_st_ref_set(x_3, x_43, x_29);
+x_45 = lean_ctor_get(x_44, 1);
+lean_inc(x_45);
+if (lean_is_exclusive(x_44)) {
+ lean_ctor_release(x_44, 0);
+ lean_ctor_release(x_44, 1);
+ x_46 = x_44;
+} else {
+ lean_dec_ref(x_44);
+ x_46 = lean_box(0);
+}
+x_47 = lean_box(0);
+if (lean_is_scalar(x_46)) {
+ x_48 = lean_alloc_ctor(0, 2, 0);
+} else {
  x_48 = x_46;
-} else {
- lean_dec_ref(x_46);
- x_48 = lean_box(0);
 }
-x_49 = lean_box(0);
-if (lean_is_scalar(x_48)) {
- x_50 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_50 = x_48;
-}
-lean_ctor_set(x_50, 0, x_49);
-lean_ctor_set(x_50, 1, x_47);
-return x_50;
+lean_ctor_set(x_48, 0, x_47);
+lean_ctor_set(x_48, 1, x_45);
+return x_48;
 }
 }
 else
 {
-uint8_t x_51; 
+uint8_t x_49; 
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_2);
 lean_dec(x_1);
-x_51 = !lean_is_exclusive(x_10);
-if (x_51 == 0)
+x_49 = !lean_is_exclusive(x_10);
+if (x_49 == 0)
 {
 return x_10;
 }
 else
 {
-lean_object* x_52; lean_object* x_53; lean_object* x_54; 
-x_52 = lean_ctor_get(x_10, 0);
-x_53 = lean_ctor_get(x_10, 1);
-lean_inc(x_53);
-lean_inc(x_52);
+lean_object* x_50; lean_object* x_51; lean_object* x_52; 
+x_50 = lean_ctor_get(x_10, 0);
+x_51 = lean_ctor_get(x_10, 1);
+lean_inc(x_51);
+lean_inc(x_50);
 lean_dec(x_10);
-x_54 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_54, 0, x_52);
-lean_ctor_set(x_54, 1, x_53);
-return x_54;
+x_52 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_52, 0, x_50);
+lean_ctor_set(x_52, 1, x_51);
+return x_52;
 }
 }
 }

stage0/stdlib/Lean/Server/Requests.c

@@ -64,7 +64,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_RequestM_readDoc___rarg(lean_object*, lea
 LEAN_EXPORT uint8_t l_Std_PersistentHashMap_containsAux___at_Lean_Server_registerLspRequestHandler___spec__7(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_Server_Snapshots_Snapshot_runTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_chainLspRequestHandler___lambda__1(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121_(lean_object*);
 LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_chainLspRequestHandler___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_map___rarg(lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
@@ -113,20 +113,21 @@ LEAN_EXPORT lean_object* l_Lean_Server_RequestM_mapTask___rarg(lean_object*, lea
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Server_lookupLspRequestHandler___spec__2(lean_object*, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_instMonadLiftIORequestM___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_withWaitFindSnapAtPos___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__2;
 size_t lean_usize_mul(size_t, size_t);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_containsAux___at_Lean_Server_registerLspRequestHandler___spec__7___boxed(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__2;
 extern lean_object* l_Task_Priority_default;
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_bindWaitFindSnap___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_String_decEq___boxed(lean_object*, lean_object*);
 size_t lean_usize_land(size_t, size_t);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Server_registerLspRequestHandler___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__5;
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Server_registerLspRequestHandler___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Server_lookupLspRequestHandler___spec__1(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Server_RequestTask_pure(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_instMonadLiftIORequestM(lean_object*);
 lean_object* lean_io_bind_task(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_asTask(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Server_RequestTask_pure___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_bindTask___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Snapshots_Snapshot_runCommandElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_waitFindSnapAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -134,26 +135,27 @@ LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___lambda__1(lea
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 uint8_t lean_usize_dec_le(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_runCommandElabM(lean_object*);
-static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__1;
-static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__3;
+static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__1;
 LEAN_EXPORT lean_object* l_Lean_Server_RequestError_fileChanged;
+static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__5;
 static lean_object* l_Lean_Server_chainLspRequestHandler___lambda__1___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Server_chainLspRequestHandler___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Snapshots_Snapshot_endPos(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_instInhabitedRequestError;
-lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_IO_AsyncList_waitFind_x3f___rarg(lean_object*, lean_object*);
 lean_object* l_instBEq___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_withWaitFindSnap___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_runCoreM(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_runTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_bindWaitFindSnap(lean_object*);
+static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__3;
 static lean_object* l_Lean_Server_chainLspRequestHandler___lambda__1___closed__2;
+static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__4;
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_withWaitFindSnapAtPos___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_registerLspRequestHandler___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_registerLspRequestHandler___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__4;
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_asTask___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_RequestM_asTask___spec__1(lean_object*);
 static lean_object* l_Lean_Server_RequestError_fileChanged___closed__2;
@@ -494,6 +496,24 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Server_parseRequestParams___rarg), 2, 0)
 return x_2;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_Server_RequestTask_pure___rarg(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+x_3 = lean_task_pure(x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Server_RequestTask_pure(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Server_RequestTask_pure___rarg), 1, 0);
+return x_2;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_Server_instMonadLiftIORequestM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -1135,21 +1155,16 @@ return x_2;
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_withWaitFindSnap___rarg(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; lean_object* x_11; lean_object* x_12; 
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
 x_7 = lean_ctor_get(x_1, 1);
 lean_inc(x_7);
 lean_dec(x_1);
-x_8 = l_IO_AsyncList_waitFind_x3f___rarg(x_2, x_7, x_6);
-x_9 = lean_ctor_get(x_8, 0);
-lean_inc(x_9);
-x_10 = lean_ctor_get(x_8, 1);
-lean_inc(x_10);
-lean_dec(x_8);
-x_11 = lean_alloc_closure((void*)(l_Lean_Server_RequestM_waitFindSnapAux___rarg), 5, 2);
-lean_closure_set(x_11, 0, x_3);
-lean_closure_set(x_11, 1, x_4);
-x_12 = l_Lean_Server_RequestM_mapTask___rarg(x_9, x_11, x_5, x_10);
-return x_12;
+x_8 = l_IO_AsyncList_waitFind_x3f___rarg(x_2, x_7);
+x_9 = lean_alloc_closure((void*)(l_Lean_Server_RequestM_waitFindSnapAux___rarg), 5, 2);
+lean_closure_set(x_9, 0, x_3);
+lean_closure_set(x_9, 1, x_4);
+x_10 = l_Lean_Server_RequestM_mapTask___rarg(x_8, x_9, x_5, x_6);
+return x_10;
 }
 }
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_withWaitFindSnap(lean_object* x_1) {
@@ -1163,21 +1178,16 @@ return x_2;
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_bindWaitFindSnap___rarg(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; lean_object* x_11; lean_object* x_12; 
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
 x_7 = lean_ctor_get(x_1, 1);
 lean_inc(x_7);
 lean_dec(x_1);
-x_8 = l_IO_AsyncList_waitFind_x3f___rarg(x_2, x_7, x_6);
-x_9 = lean_ctor_get(x_8, 0);
-lean_inc(x_9);
-x_10 = lean_ctor_get(x_8, 1);
-lean_inc(x_10);
-lean_dec(x_8);
-x_11 = lean_alloc_closure((void*)(l_Lean_Server_RequestM_waitFindSnapAux___rarg), 5, 2);
-lean_closure_set(x_11, 0, x_3);
-lean_closure_set(x_11, 1, x_4);
-x_12 = l_Lean_Server_RequestM_bindTask___rarg(x_9, x_11, x_5, x_10);
-return x_12;
+x_8 = l_IO_AsyncList_waitFind_x3f___rarg(x_2, x_7);
+x_9 = lean_alloc_closure((void*)(l_Lean_Server_RequestM_waitFindSnapAux___rarg), 5, 2);
+lean_closure_set(x_9, 0, x_3);
+lean_closure_set(x_9, 1, x_4);
+x_10 = l_Lean_Server_RequestM_bindTask___rarg(x_8, x_9, x_5, x_6);
+return x_10;
 }
 }
 LEAN_EXPORT lean_object* l_Lean_Server_RequestM_bindWaitFindSnap(lean_object* x_1) {
@@ -1787,7 +1797,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Server_RequestM_runTermElabM___rarg), 4,
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__1() {
+static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -1795,17 +1805,17 @@ x_1 = lean_alloc_closure((void*)(l_String_decEq___boxed), 2, 0);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__2() {
+static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__1;
+x_1 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__1;
 x_2 = lean_alloc_closure((void*)(l_instBEq___rarg), 3, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__3() {
+static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -1813,21 +1823,21 @@ x_1 = l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__4() {
+static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__3;
+x_1 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__3;
 x_2 = lean_alloc_ctor(0, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__5() {
+static lean_object* _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__4;
+x_1 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__4;
 x_2 = lean_unsigned_to_nat(0u);
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
@@ -1835,11 +1845,11 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; uint8_t x_4; 
-x_2 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__5;
+x_2 = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__5;
 x_3 = lean_st_mk_ref(x_2, x_1);
 x_4 = !lean_is_exclusive(x_3);
 if (x_4 == 0)
@@ -3984,17 +3994,17 @@ l_Lean_Server_RequestM_withWaitFindSnapAtPos___rarg___closed__3 = _init_l_Lean_S
 lean_mark_persistent(l_Lean_Server_RequestM_withWaitFindSnapAtPos___rarg___closed__3);
 l_Lean_Server_RequestM_withWaitFindSnapAtPos___rarg___closed__4 = _init_l_Lean_Server_RequestM_withWaitFindSnapAtPos___rarg___closed__4();
 lean_mark_persistent(l_Lean_Server_RequestM_withWaitFindSnapAtPos___rarg___closed__4);
-l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__1 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__1();
-lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__1);
-l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__2 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__2();
-lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__2);
-l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__3 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__3();
-lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__3);
-l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__4 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__4();
-lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__4);
-l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__5 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__5();
-lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125____closed__5);
-if (builtin) {res = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1125_(lean_io_mk_world());
+l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__1 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__1();
+lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__1);
+l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__2 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__2();
+lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__2);
+l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__3 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__3();
+lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__3);
+l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__4 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__4();
+lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__4);
+l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__5 = _init_l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__5();
+lean_mark_persistent(l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121____closed__5);
+if (builtin) {res = l_Lean_Server_initFn____x40_Lean_Server_Requests___hyg_1121_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 l_Lean_Server_requestHandlers = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_Server_requestHandlers);