diff --git a/stage0/src/Lean/Compiler/IR.lean b/stage0/src/Lean/Compiler/IR.lean
index e9412fed3b..8a1dbbaec8 100644
--- a/stage0/src/Lean/Compiler/IR.lean
+++ b/stage0/src/Lean/Compiler/IR.lean
@@ -20,6 +20,7 @@ import Lean.Compiler.IR.UnboxResult
 import Lean.Compiler.IR.ElimDeadBranches
 import Lean.Compiler.IR.EmitC
 import Lean.Compiler.IR.CtorLayout
+import Lean.Compiler.IR.Sorry
 
 namespace Lean.IR
 
@@ -47,6 +48,7 @@ private def compileAux (decls : Array Decl) : CompilerM Unit := do
   logDecls `expand_reset_reuse decls
   let decls := decls.map Decl.pushProj
   logDecls `push_proj decls
+  let decls ← updateSorryDep decls
   logDecls `result decls
   checkDecls decls
   addDecls decls
diff --git a/stage0/src/Lean/Compiler/IR/CompilerM.lean b/stage0/src/Lean/Compiler/IR/CompilerM.lean
index 2c4e6f6f0f..99e9ef50fc 100644
--- a/stage0/src/Lean/Compiler/IR/CompilerM.lean
+++ b/stage0/src/Lean/Compiler/IR/CompilerM.lean
@@ -142,5 +142,11 @@ def getDecl' (n : Name) (decls : Array Decl) : CompilerM Decl := do
   let (some decl) ← findDecl' n decls | throw s!"unknown declaration '{n}'"
   pure decl
 
+@[export lean_decl_get_sorry_dep]
+def getSorryDep (env : Environment) (declName : Name) : Option Name :=
+  match (declMapExt.getState env).find? declName with
+  | some (Decl.fdecl (info := { sorryDep? := dep?, .. }) ..) => dep?
+  | _ => none
+
 end IR
 end Lean
diff --git a/stage0/src/Lean/Compiler/IR/Sorry.lean b/stage0/src/Lean/Compiler/IR/Sorry.lean
new file mode 100644
index 0000000000..0536b07d74
--- /dev/null
+++ b/stage0/src/Lean/Compiler/IR/Sorry.lean
@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Compiler.IR.CompilerM
+
+namespace Lean.IR
+namespace Sorry
+
+structure State where
+  localSorryMap : NameMap Name := {}
+  modified : Bool := false
+
+abbrev M := StateT State CompilerM
+
+def visitExpr : Expr → ExceptT Name M Unit
+  | Expr.fap f _  => getSorryDepFor? f
+  | Expr.pap f _  => getSorryDepFor? f
+  | _             => return ()
+where
+  getSorryDepFor? (f : Name) : ExceptT Name M Unit := do
+    let found (g : Name) :=
+      if g == ``sorryAx then
+        throw f
+      else
+        throw g
+    if f == ``sorryAx then
+      throw f
+    else if let some g := (← get).localSorryMap.find? f then
+      found g
+    else match (← findDecl f) with
+      | Decl.fdecl (info := { sorryDep? := some g, .. }) .. => found g
+      | _ => return ()
+
+partial def visitFndBody (b : FnBody) : ExceptT Name M Unit := do
+  match b with
+  | FnBody.vdecl _ _ v b   => visitExpr v; visitFndBody b
+  | FnBody.jdecl _ _ v b   => visitFndBody v; visitFndBody b
+  | FnBody.case _ _ _ alts => alts.forM fun alt => visitFndBody alt.body
+  | _ =>
+    unless b.isTerminal do
+      let (instr, b) := b.split
+      visitFndBody b
+
+def visitDecl (d : Decl) : M Unit := do
+  match d with
+  | Decl.fdecl (f := f) (body := b) .. =>
+    match (← get).localSorryMap.find? f with
+    | some _ => return ()
+    | none =>
+      match (← visitFndBody b |>.run) with
+      | Except.ok _    => return ()
+      | Except.error g =>
+        modify fun s => {
+          localSorryMap := s.localSorryMap.insert f g
+          modified      := true
+        }
+  | _ => return ()
+
+partial def collect (decls : Array Decl) : M Unit := do
+  modify fun s => { s with modified := false }
+  decls.forM visitDecl
+  if (← get).modified then
+    collect decls
+
+end Sorry
+
+def updateSorryDep (decls : Array Decl) : CompilerM (Array Decl) := do
+  let (_, s) ← Sorry.collect decls |>.run {}
+  return decls.map fun decl =>
+    match decl with
+    | Decl.fdecl f xs t b info =>
+      match s.localSorryMap.find? f with
+      | some g => Decl.fdecl f xs t b { info with sorryDep? := some g }
+      | _ => decl
+    | _ => decl
+
+end Lean.IR
diff --git a/stage0/src/library/compiler/ir_interpreter.cpp b/stage0/src/library/compiler/ir_interpreter.cpp
index d3e0c3037c..a6e907aba1 100644
--- a/stage0/src/library/compiler/ir_interpreter.cpp
+++ b/stage0/src/library/compiler/ir_interpreter.cpp
@@ -1004,7 +1004,16 @@ public:
     }
 };
 
+extern "C" object * lean_decl_get_sorry_dep(object * env, object * n);
+
+optional<name> get_sorry_dep(environment const & env, name const & n) {
+    return option_ref<name>(lean_decl_get_sorry_dep(env.to_obj_arg(), n.to_obj_arg())).get();
+}
+
 object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args) {
+    if (get_sorry_dep(env, fn)) {
+        throw exception("cannot evaluate code because it uses 'sorry' and/or contains errors");
+    }
     return interpreter::with_interpreter<object *>(env, opts, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); });
 }
 uint32 run_main(environment const & env, options const & opts, int argv, char * argc[]) {
diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt
index 1c96579296..758e2316cc 100644
--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
@@ -1 +1 @@
-add_library (stage0 OBJECT ./Init.c ./Init/Classical.c ./Init/Coe.c ./Init/Control.c ./Init/Control/Basic.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Id.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Control/StateRef.c ./Init/Core.c ./Init/Data.c ./Init/Data/Array.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/InsertionSort.c ./Init/Data/Array/QSort.c ./Init/Data/Array/Subarray.c ./Init/Data/Basic.c ./Init/Data/ByteArray.c ./Init/Data/ByteArray/Basic.c ./Init/Data/Char.c ./Init/Data/Char/Basic.c ./Init/Data/Fin.c ./Init/Data/Fin/Basic.c ./Init/Data/Float.c ./Init/Data/FloatArray.c ./Init/Data/FloatArray/Basic.c ./Init/Data/Format.c ./Init/Data/Format/Basic.c ./Init/Data/Format/Instances.c ./Init/Data/Format/Macro.c ./Init/Data/Hashable.c ./Init/Data/Int.c ./Init/Data/Int/Basic.c ./Init/Data/List.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Control.c ./Init/Data/Nat.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.c ./Init/Data/Nat/Div.c ./Init/Data/OfScientific.c ./Init/Data/Option.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Instances.c ./Init/Data/Random.c ./Init/Data/Range.c ./Init/Data/Repr.c ./Init/Data/Stream.c ./Init/Data/String.c ./Init/Data/String/Basic.c ./Init/Data/String/Extra.c ./Init/Data/ToString.c ./Init/Data/ToString/Basic.c ./Init/Data/ToString/Macro.c ./Init/Data/UInt.c ./Init/Fix.c ./Init/Meta.c ./Init/Notation.c ./Init/NotationExtra.c ./Init/Prelude.c ./Init/SimpLemmas.c ./Init/SizeOf.c ./Init/System.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/IOError.c ./Init/System/Platform.c ./Init/System/ST.c ./Init/Util.c ./Init/WF.c ./Lean.c ./Lean/Attributes.c ./Lean/AuxRecursor.c ./Lean/Class.c ./Lean/Compiler.c ./Lean/Compiler/BorrowedAnnotation.c ./Lean/Compiler/ClosedTermCache.c ./Lean/Compiler/ConstFolding.c ./Lean/Compiler/ExportAttr.c ./Lean/Compiler/ExternAttr.c ./Lean/Compiler/IR.c ./Lean/Compiler/IR/Basic.c ./Lean/Compiler/IR/Borrow.c ./Lean/Compiler/IR/Boxing.c ./Lean/Compiler/IR/Checker.c ./Lean/Compiler/IR/CompilerM.c ./Lean/Compiler/IR/CtorLayout.c ./Lean/Compiler/IR/ElimDeadBranches.c ./Lean/Compiler/IR/ElimDeadVars.c ./Lean/Compiler/IR/EmitC.c ./Lean/Compiler/IR/EmitUtil.c ./Lean/Compiler/IR/ExpandResetReuse.c ./Lean/Compiler/IR/Format.c ./Lean/Compiler/IR/FreeVars.c ./Lean/Compiler/IR/LiveVars.c ./Lean/Compiler/IR/NormIds.c ./Lean/Compiler/IR/PushProj.c ./Lean/Compiler/IR/RC.c ./Lean/Compiler/IR/ResetReuse.c ./Lean/Compiler/IR/SimpCase.c ./Lean/Compiler/IR/UnboxResult.c ./Lean/Compiler/ImplementedByAttr.c ./Lean/Compiler/InitAttr.c ./Lean/Compiler/InlineAttrs.c ./Lean/Compiler/NameMangling.c ./Lean/Compiler/NeverExtractAttr.c ./Lean/Compiler/Specialize.c ./Lean/Compiler/Util.c ./Lean/CoreM.c ./Lean/Data.c ./Lean/Data/Format.c ./Lean/Data/Json.c ./Lean/Data/Json/Basic.c ./Lean/Data/Json/FromToJson.c ./Lean/Data/Json/Parser.c ./Lean/Data/Json/Printer.c ./Lean/Data/Json/Stream.c ./Lean/Data/JsonRpc.c ./Lean/Data/KVMap.c ./Lean/Data/LBool.c ./Lean/Data/LOption.c ./Lean/Data/Lsp.c ./Lean/Data/Lsp/Basic.c ./Lean/Data/Lsp/Capabilities.c ./Lean/Data/Lsp/Communication.c ./Lean/Data/Lsp/Diagnostics.c ./Lean/Data/Lsp/Extra.c ./Lean/Data/Lsp/InitShutdown.c ./Lean/Data/Lsp/Ipc.c ./Lean/Data/Lsp/LanguageFeatures.c ./Lean/Data/Lsp/TextSync.c ./Lean/Data/Lsp/Utf16.c ./Lean/Data/Lsp/Workspace.c ./Lean/Data/Name.c ./Lean/Data/NameTrie.c ./Lean/Data/Occurrences.c ./Lean/Data/OpenDecl.c ./Lean/Data/Options.c ./Lean/Data/Position.c ./Lean/Data/PrefixTree.c ./Lean/Data/SMap.c ./Lean/Data/Trie.c ./Lean/Declaration.c ./Lean/DeclarationRange.c ./Lean/DocString.c ./Lean/Elab.c ./Lean/Elab/App.c ./Lean/Elab/Attributes.c ./Lean/Elab/AutoBound.c ./Lean/Elab/Binders.c ./Lean/Elab/BuiltinNotation.c ./Lean/Elab/CollectFVars.c ./Lean/Elab/Command.c ./Lean/Elab/DeclModifiers.c ./Lean/Elab/DeclUtil.c ./Lean/Elab/Declaration.c ./Lean/Elab/DeclarationRange.c ./Lean/Elab/DefView.c ./Lean/Elab/Deriving.c ./Lean/Elab/Deriving/BEq.c ./Lean/Elab/Deriving/Basic.c ./Lean/Elab/Deriving/DecEq.c ./Lean/Elab/Deriving/FromToJson.c ./Lean/Elab/Deriving/Inhabited.c ./Lean/Elab/Deriving/Repr.c ./Lean/Elab/Deriving/SizeOf.c ./Lean/Elab/Deriving/Util.c ./Lean/Elab/Do.c ./Lean/Elab/Exception.c ./Lean/Elab/Frontend.c ./Lean/Elab/Import.c ./Lean/Elab/Inductive.c ./Lean/Elab/InfoTree.c ./Lean/Elab/LetRec.c ./Lean/Elab/Level.c ./Lean/Elab/Log.c ./Lean/Elab/Match.c ./Lean/Elab/MutualDef.c ./Lean/Elab/PreDefinition.c ./Lean/Elab/PreDefinition/Basic.c ./Lean/Elab/PreDefinition/Main.c ./Lean/Elab/PreDefinition/MkInhabitant.c ./Lean/Elab/PreDefinition/Structural.c ./Lean/Elab/PreDefinition/WF.c ./Lean/Elab/Print.c ./Lean/Elab/Quotation.c ./Lean/Elab/Quotation/Util.c ./Lean/Elab/StructInst.c ./Lean/Elab/Structure.c ./Lean/Elab/Syntax.c ./Lean/Elab/SyntheticMVars.c ./Lean/Elab/Tactic.c ./Lean/Elab/Tactic/Basic.c ./Lean/Elab/Tactic/Binders.c ./Lean/Elab/Tactic/ElabTerm.c ./Lean/Elab/Tactic/Generalize.c ./Lean/Elab/Tactic/Induction.c ./Lean/Elab/Tactic/Injection.c ./Lean/Elab/Tactic/Location.c ./Lean/Elab/Tactic/Match.c ./Lean/Elab/Tactic/Rewrite.c ./Lean/Elab/Tactic/Simp.c ./Lean/Elab/Term.c ./Lean/Elab/Util.c ./Lean/Environment.c ./Lean/Eval.c ./Lean/Exception.c ./Lean/Expr.c ./Lean/HeadIndex.c ./Lean/Hygiene.c ./Lean/InternalExceptionId.c ./Lean/KeyedDeclsAttribute.c ./Lean/Level.c ./Lean/LocalContext.c ./Lean/Message.c ./Lean/Meta.c ./Lean/Meta/AbstractMVars.c ./Lean/Meta/AbstractNestedProofs.c ./Lean/Meta/AppBuilder.c ./Lean/Meta/Basic.c ./Lean/Meta/Check.c ./Lean/Meta/Closure.c ./Lean/Meta/CollectMVars.c ./Lean/Meta/DiscrTree.c ./Lean/Meta/DiscrTreeTypes.c ./Lean/Meta/ExprDefEq.c ./Lean/Meta/ForEachExpr.c ./Lean/Meta/FunInfo.c ./Lean/Meta/GeneralizeTelescope.c ./Lean/Meta/GetConst.c ./Lean/Meta/Inductive.c ./Lean/Meta/InferType.c ./Lean/Meta/Instances.c ./Lean/Meta/KAbstract.c ./Lean/Meta/LevelDefEq.c ./Lean/Meta/Match.c ./Lean/Meta/Match/Basic.c ./Lean/Meta/Match/CaseArraySizes.c ./Lean/Meta/Match/CaseValues.c ./Lean/Meta/Match/MVarRenaming.c ./Lean/Meta/Match/Match.c ./Lean/Meta/Match/MatchPatternAttr.c ./Lean/Meta/Match/MatcherInfo.c ./Lean/Meta/MatchUtil.c ./Lean/Meta/Offset.c ./Lean/Meta/PPGoal.c ./Lean/Meta/RecursorInfo.c ./Lean/Meta/Reduce.c ./Lean/Meta/ReduceEval.c ./Lean/Meta/SizeOf.c ./Lean/Meta/SynthInstance.c ./Lean/Meta/Tactic.c ./Lean/Meta/Tactic/Apply.c ./Lean/Meta/Tactic/Assert.c ./Lean/Meta/Tactic/Assumption.c ./Lean/Meta/Tactic/Cases.c ./Lean/Meta/Tactic/Clear.c ./Lean/Meta/Tactic/Constructor.c ./Lean/Meta/Tactic/Delta.c ./Lean/Meta/Tactic/ElimInfo.c ./Lean/Meta/Tactic/FVarSubst.c ./Lean/Meta/Tactic/Generalize.c ./Lean/Meta/Tactic/Induction.c ./Lean/Meta/Tactic/Injection.c ./Lean/Meta/Tactic/Intro.c ./Lean/Meta/Tactic/Replace.c ./Lean/Meta/Tactic/Revert.c ./Lean/Meta/Tactic/Rewrite.c ./Lean/Meta/Tactic/Simp.c ./Lean/Meta/Tactic/Simp/Main.c ./Lean/Meta/Tactic/Simp/Rewrite.c ./Lean/Meta/Tactic/Simp/SimpLemmas.c ./Lean/Meta/Tactic/Simp/Types.c ./Lean/Meta/Tactic/Subst.c ./Lean/Meta/Tactic/Util.c ./Lean/Meta/Transform.c ./Lean/Meta/TransparencyMode.c ./Lean/Meta/UnificationHint.c ./Lean/Meta/WHNF.c ./Lean/MetavarContext.c ./Lean/Modifiers.c ./Lean/MonadEnv.c ./Lean/Parser.c ./Lean/Parser/Attr.c ./Lean/Parser/Basic.c ./Lean/Parser/Command.c ./Lean/Parser/Do.c ./Lean/Parser/Extension.c ./Lean/Parser/Extra.c ./Lean/Parser/Level.c ./Lean/Parser/Module.c ./Lean/Parser/StrInterpolation.c ./Lean/Parser/Syntax.c ./Lean/Parser/Tactic.c ./Lean/Parser/Term.c ./Lean/ParserCompiler.c ./Lean/ParserCompiler/Attribute.c ./Lean/PrettyPrinter.c ./Lean/PrettyPrinter/Basic.c ./Lean/PrettyPrinter/Delaborator.c ./Lean/PrettyPrinter/Delaborator/Basic.c ./Lean/PrettyPrinter/Delaborator/Builtins.c ./Lean/PrettyPrinter/Formatter.c ./Lean/PrettyPrinter/Parenthesizer.c ./Lean/ProjFns.c ./Lean/ReducibilityAttrs.c ./Lean/ResolveName.c ./Lean/Runtime.c ./Lean/ScopedEnvExtension.c ./Lean/Server.c ./Lean/Server/AsyncList.c ./Lean/Server/FileSource.c ./Lean/Server/FileWorker.c ./Lean/Server/InfoUtils.c ./Lean/Server/Snapshots.c ./Lean/Server/Utils.c ./Lean/Server/Watchdog.c ./Lean/Structure.c ./Lean/Syntax.c ./Lean/ToExpr.c ./Lean/Util.c ./Lean/Util/CollectFVars.c ./Lean/Util/CollectLevelParams.c ./Lean/Util/CollectMVars.c ./Lean/Util/Constructions.c ./Lean/Util/FindExpr.c ./Lean/Util/FindMVar.c ./Lean/Util/FoldConsts.c ./Lean/Util/ForEachExpr.c ./Lean/Util/MonadCache.c ./Lean/Util/PPExt.c ./Lean/Util/Path.c ./Lean/Util/Profile.c ./Lean/Util/RecDepth.c ./Lean/Util/Recognizers.c ./Lean/Util/ReplaceExpr.c ./Lean/Util/ReplaceLevel.c ./Lean/Util/SCC.c ./Lean/Util/Sorry.c ./Lean/Util/Trace.c ./Leanpkg.c ./Leanpkg/Git.c ./Leanpkg/LeanVersion.c ./Leanpkg/Manifest.c ./Leanpkg/Proc.c ./Leanpkg/Resolve.c ./Leanpkg/Toml.c ./Std.c ./Std/Data.c ./Std/Data/AssocList.c ./Std/Data/BinomialHeap.c ./Std/Data/DList.c ./Std/Data/HashMap.c ./Std/Data/HashSet.c ./Std/Data/PersistentArray.c ./Std/Data/PersistentHashMap.c ./Std/Data/PersistentHashSet.c ./Std/Data/Queue.c ./Std/Data/RBMap.c ./Std/Data/RBTree.c ./Std/Data/Stack.c ./Std/ShareCommon.c )
+add_library (stage0 OBJECT ./Init.c ./Init/Classical.c ./Init/Coe.c ./Init/Control.c ./Init/Control/Basic.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Id.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Control/StateRef.c ./Init/Core.c ./Init/Data.c ./Init/Data/Array.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/InsertionSort.c ./Init/Data/Array/QSort.c ./Init/Data/Array/Subarray.c ./Init/Data/Basic.c ./Init/Data/ByteArray.c ./Init/Data/ByteArray/Basic.c ./Init/Data/Char.c ./Init/Data/Char/Basic.c ./Init/Data/Fin.c ./Init/Data/Fin/Basic.c ./Init/Data/Float.c ./Init/Data/FloatArray.c ./Init/Data/FloatArray/Basic.c ./Init/Data/Format.c ./Init/Data/Format/Basic.c ./Init/Data/Format/Instances.c ./Init/Data/Format/Macro.c ./Init/Data/Hashable.c ./Init/Data/Int.c ./Init/Data/Int/Basic.c ./Init/Data/List.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Control.c ./Init/Data/Nat.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.c ./Init/Data/Nat/Div.c ./Init/Data/OfScientific.c ./Init/Data/Option.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Instances.c ./Init/Data/Random.c ./Init/Data/Range.c ./Init/Data/Repr.c ./Init/Data/Stream.c ./Init/Data/String.c ./Init/Data/String/Basic.c ./Init/Data/String/Extra.c ./Init/Data/ToString.c ./Init/Data/ToString/Basic.c ./Init/Data/ToString/Macro.c ./Init/Data/UInt.c ./Init/Fix.c ./Init/Meta.c ./Init/Notation.c ./Init/NotationExtra.c ./Init/Prelude.c ./Init/SimpLemmas.c ./Init/SizeOf.c ./Init/System.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/IOError.c ./Init/System/Platform.c ./Init/System/ST.c ./Init/Util.c ./Init/WF.c ./Lean.c ./Lean/Attributes.c ./Lean/AuxRecursor.c ./Lean/Class.c ./Lean/Compiler.c ./Lean/Compiler/BorrowedAnnotation.c ./Lean/Compiler/ClosedTermCache.c ./Lean/Compiler/ConstFolding.c ./Lean/Compiler/ExportAttr.c ./Lean/Compiler/ExternAttr.c ./Lean/Compiler/IR.c ./Lean/Compiler/IR/Basic.c ./Lean/Compiler/IR/Borrow.c ./Lean/Compiler/IR/Boxing.c ./Lean/Compiler/IR/Checker.c ./Lean/Compiler/IR/CompilerM.c ./Lean/Compiler/IR/CtorLayout.c ./Lean/Compiler/IR/ElimDeadBranches.c ./Lean/Compiler/IR/ElimDeadVars.c ./Lean/Compiler/IR/EmitC.c ./Lean/Compiler/IR/EmitUtil.c ./Lean/Compiler/IR/ExpandResetReuse.c ./Lean/Compiler/IR/Format.c ./Lean/Compiler/IR/FreeVars.c ./Lean/Compiler/IR/LiveVars.c ./Lean/Compiler/IR/NormIds.c ./Lean/Compiler/IR/PushProj.c ./Lean/Compiler/IR/RC.c ./Lean/Compiler/IR/ResetReuse.c ./Lean/Compiler/IR/SimpCase.c ./Lean/Compiler/IR/Sorry.c ./Lean/Compiler/IR/UnboxResult.c ./Lean/Compiler/ImplementedByAttr.c ./Lean/Compiler/InitAttr.c ./Lean/Compiler/InlineAttrs.c ./Lean/Compiler/NameMangling.c ./Lean/Compiler/NeverExtractAttr.c ./Lean/Compiler/Specialize.c ./Lean/Compiler/Util.c ./Lean/CoreM.c ./Lean/Data.c ./Lean/Data/Format.c ./Lean/Data/Json.c ./Lean/Data/Json/Basic.c ./Lean/Data/Json/FromToJson.c ./Lean/Data/Json/Parser.c ./Lean/Data/Json/Printer.c ./Lean/Data/Json/Stream.c ./Lean/Data/JsonRpc.c ./Lean/Data/KVMap.c ./Lean/Data/LBool.c ./Lean/Data/LOption.c ./Lean/Data/Lsp.c ./Lean/Data/Lsp/Basic.c ./Lean/Data/Lsp/Capabilities.c ./Lean/Data/Lsp/Communication.c ./Lean/Data/Lsp/Diagnostics.c ./Lean/Data/Lsp/Extra.c ./Lean/Data/Lsp/InitShutdown.c ./Lean/Data/Lsp/Ipc.c ./Lean/Data/Lsp/LanguageFeatures.c ./Lean/Data/Lsp/TextSync.c ./Lean/Data/Lsp/Utf16.c ./Lean/Data/Lsp/Workspace.c ./Lean/Data/Name.c ./Lean/Data/NameTrie.c ./Lean/Data/Occurrences.c ./Lean/Data/OpenDecl.c ./Lean/Data/Options.c ./Lean/Data/Position.c ./Lean/Data/PrefixTree.c ./Lean/Data/SMap.c ./Lean/Data/Trie.c ./Lean/Declaration.c ./Lean/DeclarationRange.c ./Lean/DocString.c ./Lean/Elab.c ./Lean/Elab/App.c ./Lean/Elab/Attributes.c ./Lean/Elab/AutoBound.c ./Lean/Elab/Binders.c ./Lean/Elab/BuiltinNotation.c ./Lean/Elab/CollectFVars.c ./Lean/Elab/Command.c ./Lean/Elab/DeclModifiers.c ./Lean/Elab/DeclUtil.c ./Lean/Elab/Declaration.c ./Lean/Elab/DeclarationRange.c ./Lean/Elab/DefView.c ./Lean/Elab/Deriving.c ./Lean/Elab/Deriving/BEq.c ./Lean/Elab/Deriving/Basic.c ./Lean/Elab/Deriving/DecEq.c ./Lean/Elab/Deriving/FromToJson.c ./Lean/Elab/Deriving/Inhabited.c ./Lean/Elab/Deriving/Repr.c ./Lean/Elab/Deriving/SizeOf.c ./Lean/Elab/Deriving/Util.c ./Lean/Elab/Do.c ./Lean/Elab/Exception.c ./Lean/Elab/Frontend.c ./Lean/Elab/Import.c ./Lean/Elab/Inductive.c ./Lean/Elab/InfoTree.c ./Lean/Elab/LetRec.c ./Lean/Elab/Level.c ./Lean/Elab/Log.c ./Lean/Elab/Match.c ./Lean/Elab/MutualDef.c ./Lean/Elab/PreDefinition.c ./Lean/Elab/PreDefinition/Basic.c ./Lean/Elab/PreDefinition/Main.c ./Lean/Elab/PreDefinition/MkInhabitant.c ./Lean/Elab/PreDefinition/Structural.c ./Lean/Elab/PreDefinition/WF.c ./Lean/Elab/Print.c ./Lean/Elab/Quotation.c ./Lean/Elab/Quotation/Util.c ./Lean/Elab/StructInst.c ./Lean/Elab/Structure.c ./Lean/Elab/Syntax.c ./Lean/Elab/SyntheticMVars.c ./Lean/Elab/Tactic.c ./Lean/Elab/Tactic/Basic.c ./Lean/Elab/Tactic/Binders.c ./Lean/Elab/Tactic/ElabTerm.c ./Lean/Elab/Tactic/Generalize.c ./Lean/Elab/Tactic/Induction.c ./Lean/Elab/Tactic/Injection.c ./Lean/Elab/Tactic/Location.c ./Lean/Elab/Tactic/Match.c ./Lean/Elab/Tactic/Rewrite.c ./Lean/Elab/Tactic/Simp.c ./Lean/Elab/Term.c ./Lean/Elab/Util.c ./Lean/Environment.c ./Lean/Eval.c ./Lean/Exception.c ./Lean/Expr.c ./Lean/HeadIndex.c ./Lean/Hygiene.c ./Lean/InternalExceptionId.c ./Lean/KeyedDeclsAttribute.c ./Lean/Level.c ./Lean/LocalContext.c ./Lean/Message.c ./Lean/Meta.c ./Lean/Meta/AbstractMVars.c ./Lean/Meta/AbstractNestedProofs.c ./Lean/Meta/AppBuilder.c ./Lean/Meta/Basic.c ./Lean/Meta/Check.c ./Lean/Meta/Closure.c ./Lean/Meta/CollectMVars.c ./Lean/Meta/DiscrTree.c ./Lean/Meta/DiscrTreeTypes.c ./Lean/Meta/ExprDefEq.c ./Lean/Meta/ForEachExpr.c ./Lean/Meta/FunInfo.c ./Lean/Meta/GeneralizeTelescope.c ./Lean/Meta/GetConst.c ./Lean/Meta/Inductive.c ./Lean/Meta/InferType.c ./Lean/Meta/Instances.c ./Lean/Meta/KAbstract.c ./Lean/Meta/LevelDefEq.c ./Lean/Meta/Match.c ./Lean/Meta/Match/Basic.c ./Lean/Meta/Match/CaseArraySizes.c ./Lean/Meta/Match/CaseValues.c ./Lean/Meta/Match/MVarRenaming.c ./Lean/Meta/Match/Match.c ./Lean/Meta/Match/MatchPatternAttr.c ./Lean/Meta/Match/MatcherInfo.c ./Lean/Meta/MatchUtil.c ./Lean/Meta/Offset.c ./Lean/Meta/PPGoal.c ./Lean/Meta/RecursorInfo.c ./Lean/Meta/Reduce.c ./Lean/Meta/ReduceEval.c ./Lean/Meta/SizeOf.c ./Lean/Meta/SynthInstance.c ./Lean/Meta/Tactic.c ./Lean/Meta/Tactic/Apply.c ./Lean/Meta/Tactic/Assert.c ./Lean/Meta/Tactic/Assumption.c ./Lean/Meta/Tactic/Cases.c ./Lean/Meta/Tactic/Clear.c ./Lean/Meta/Tactic/Constructor.c ./Lean/Meta/Tactic/Delta.c ./Lean/Meta/Tactic/ElimInfo.c ./Lean/Meta/Tactic/FVarSubst.c ./Lean/Meta/Tactic/Generalize.c ./Lean/Meta/Tactic/Induction.c ./Lean/Meta/Tactic/Injection.c ./Lean/Meta/Tactic/Intro.c ./Lean/Meta/Tactic/Replace.c ./Lean/Meta/Tactic/Revert.c ./Lean/Meta/Tactic/Rewrite.c ./Lean/Meta/Tactic/Simp.c ./Lean/Meta/Tactic/Simp/Main.c ./Lean/Meta/Tactic/Simp/Rewrite.c ./Lean/Meta/Tactic/Simp/SimpLemmas.c ./Lean/Meta/Tactic/Simp/Types.c ./Lean/Meta/Tactic/Subst.c ./Lean/Meta/Tactic/Util.c ./Lean/Meta/Transform.c ./Lean/Meta/TransparencyMode.c ./Lean/Meta/UnificationHint.c ./Lean/Meta/WHNF.c ./Lean/MetavarContext.c ./Lean/Modifiers.c ./Lean/MonadEnv.c ./Lean/Parser.c ./Lean/Parser/Attr.c ./Lean/Parser/Basic.c ./Lean/Parser/Command.c ./Lean/Parser/Do.c ./Lean/Parser/Extension.c ./Lean/Parser/Extra.c ./Lean/Parser/Level.c ./Lean/Parser/Module.c ./Lean/Parser/StrInterpolation.c ./Lean/Parser/Syntax.c ./Lean/Parser/Tactic.c ./Lean/Parser/Term.c ./Lean/ParserCompiler.c ./Lean/ParserCompiler/Attribute.c ./Lean/PrettyPrinter.c ./Lean/PrettyPrinter/Basic.c ./Lean/PrettyPrinter/Delaborator.c ./Lean/PrettyPrinter/Delaborator/Basic.c ./Lean/PrettyPrinter/Delaborator/Builtins.c ./Lean/PrettyPrinter/Formatter.c ./Lean/PrettyPrinter/Parenthesizer.c ./Lean/ProjFns.c ./Lean/ReducibilityAttrs.c ./Lean/ResolveName.c ./Lean/Runtime.c ./Lean/ScopedEnvExtension.c ./Lean/Server.c ./Lean/Server/AsyncList.c ./Lean/Server/FileSource.c ./Lean/Server/FileWorker.c ./Lean/Server/InfoUtils.c ./Lean/Server/Snapshots.c ./Lean/Server/Utils.c ./Lean/Server/Watchdog.c ./Lean/Structure.c ./Lean/Syntax.c ./Lean/ToExpr.c ./Lean/Util.c ./Lean/Util/CollectFVars.c ./Lean/Util/CollectLevelParams.c ./Lean/Util/CollectMVars.c ./Lean/Util/Constructions.c ./Lean/Util/FindExpr.c ./Lean/Util/FindMVar.c ./Lean/Util/FoldConsts.c ./Lean/Util/ForEachExpr.c ./Lean/Util/MonadCache.c ./Lean/Util/PPExt.c ./Lean/Util/Path.c ./Lean/Util/Profile.c ./Lean/Util/RecDepth.c ./Lean/Util/Recognizers.c ./Lean/Util/ReplaceExpr.c ./Lean/Util/ReplaceLevel.c ./Lean/Util/SCC.c ./Lean/Util/Sorry.c ./Lean/Util/Trace.c ./Leanpkg.c ./Leanpkg/Git.c ./Leanpkg/LeanVersion.c ./Leanpkg/Manifest.c ./Leanpkg/Proc.c ./Leanpkg/Resolve.c ./Leanpkg/Toml.c ./Std.c ./Std/Data.c ./Std/Data/AssocList.c ./Std/Data/BinomialHeap.c ./Std/Data/DList.c ./Std/Data/HashMap.c ./Std/Data/HashSet.c ./Std/Data/PersistentArray.c ./Std/Data/PersistentHashMap.c ./Std/Data/PersistentHashSet.c ./Std/Data/Queue.c ./Std/Data/RBMap.c ./Std/Data/RBTree.c ./Std/Data/Stack.c ./Std/ShareCommon.c )
diff --git a/stage0/stdlib/Lean/Compiler/IR.c b/stage0/stdlib/Lean/Compiler/IR.c
index e4c458d7c8..3ce39be623 100644
--- a/stage0/stdlib/Lean/Compiler/IR.c
+++ b/stage0/stdlib/Lean/Compiler/IR.c
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Compiler.IR
-// Imports: Init Lean.Compiler.IR.Basic Lean.Compiler.IR.Format Lean.Compiler.IR.CompilerM Lean.Compiler.IR.PushProj Lean.Compiler.IR.ElimDeadVars Lean.Compiler.IR.SimpCase Lean.Compiler.IR.ResetReuse Lean.Compiler.IR.NormIds Lean.Compiler.IR.Checker Lean.Compiler.IR.Borrow Lean.Compiler.IR.Boxing Lean.Compiler.IR.RC Lean.Compiler.IR.ExpandResetReuse Lean.Compiler.IR.UnboxResult Lean.Compiler.IR.ElimDeadBranches Lean.Compiler.IR.EmitC Lean.Compiler.IR.CtorLayout
+// Imports: Init Lean.Compiler.IR.Basic Lean.Compiler.IR.Format Lean.Compiler.IR.CompilerM Lean.Compiler.IR.PushProj Lean.Compiler.IR.ElimDeadVars Lean.Compiler.IR.SimpCase Lean.Compiler.IR.ResetReuse Lean.Compiler.IR.NormIds Lean.Compiler.IR.Checker Lean.Compiler.IR.Borrow Lean.Compiler.IR.Boxing Lean.Compiler.IR.RC Lean.Compiler.IR.ExpandResetReuse Lean.Compiler.IR.UnboxResult Lean.Compiler.IR.ElimDeadBranches Lean.Compiler.IR.EmitC Lean.Compiler.IR.CtorLayout Lean.Compiler.IR.Sorry
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -76,6 +76,7 @@ lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__2;
 lean_object* l_Lean_IR_Decl_simpCase(lean_object*);
 lean_object* l_Lean_IR_Decl_expandResetReuse(lean_object*);
 lean_object* l_Lean_IR_elimDeadBranches(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_updateSorryDep(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__21;
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Compiler_IR_0__Lean_IR_compileAux___spec__5(size_t, size_t, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@@ -583,7 +584,7 @@ lean_inc(x_1);
 x_8 = l_Lean_IR_checkDecls(x_1, x_2, x_7);
 if (lean_obj_tag(x_8) == 0)
 {
-lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; size_t x_18; size_t 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; size_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; size_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; size_t x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; size_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; 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; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; size_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; size_t x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; 
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; size_t x_18; size_t 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; size_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; size_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; size_t x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; size_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; 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; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; size_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; size_t x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; 
 x_9 = lean_ctor_get(x_8, 1);
 lean_inc(x_9);
 lean_dec(x_8);
@@ -722,70 +723,76 @@ x_94 = l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux(x_23, x_24,
 x_95 = lean_ctor_get(x_94, 1);
 lean_inc(x_95);
 lean_dec(x_94);
-x_96 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__31;
-x_97 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__30;
-lean_inc(x_93);
-x_98 = l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux(x_96, x_97, x_93, x_2, x_95);
-x_99 = lean_ctor_get(x_98, 1);
-lean_inc(x_99);
-lean_dec(x_98);
-lean_inc(x_93);
-x_100 = l_Lean_IR_checkDecls(x_93, x_2, x_99);
-if (lean_obj_tag(x_100) == 0)
+x_96 = l_Lean_IR_updateSorryDep(x_93, x_2, x_95);
+x_97 = lean_ctor_get(x_96, 0);
+lean_inc(x_97);
+x_98 = lean_ctor_get(x_96, 1);
+lean_inc(x_98);
+lean_dec(x_96);
+x_99 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__31;
+x_100 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__30;
+lean_inc(x_97);
+x_101 = l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux(x_99, x_100, x_97, x_2, x_98);
+x_102 = lean_ctor_get(x_101, 1);
+lean_inc(x_102);
+lean_dec(x_101);
+lean_inc(x_97);
+x_103 = l_Lean_IR_checkDecls(x_97, x_2, x_102);
+if (lean_obj_tag(x_103) == 0)
 {
-lean_object* x_101; lean_object* x_102; 
-x_101 = lean_ctor_get(x_100, 1);
-lean_inc(x_101);
-lean_dec(x_100);
-x_102 = l_Lean_IR_addDecls(x_93, x_2, x_101);
-lean_dec(x_93);
-return x_102;
-}
-else
-{
-uint8_t x_103; 
-lean_dec(x_93);
-x_103 = !lean_is_exclusive(x_100);
-if (x_103 == 0)
-{
-return x_100;
-}
-else
-{
-lean_object* x_104; lean_object* x_105; lean_object* x_106; 
-x_104 = lean_ctor_get(x_100, 0);
-x_105 = lean_ctor_get(x_100, 1);
-lean_inc(x_105);
+lean_object* x_104; lean_object* x_105; 
+x_104 = lean_ctor_get(x_103, 1);
 lean_inc(x_104);
-lean_dec(x_100);
-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;
+lean_dec(x_103);
+x_105 = l_Lean_IR_addDecls(x_97, x_2, x_104);
+lean_dec(x_97);
+return x_105;
+}
+else
+{
+uint8_t x_106; 
+lean_dec(x_97);
+x_106 = !lean_is_exclusive(x_103);
+if (x_106 == 0)
+{
+return x_103;
+}
+else
+{
+lean_object* x_107; lean_object* x_108; lean_object* x_109; 
+x_107 = lean_ctor_get(x_103, 0);
+x_108 = lean_ctor_get(x_103, 1);
+lean_inc(x_108);
+lean_inc(x_107);
+lean_dec(x_103);
+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;
 }
 }
 }
 else
 {
-uint8_t x_107; 
+uint8_t x_110; 
 lean_dec(x_1);
-x_107 = !lean_is_exclusive(x_8);
-if (x_107 == 0)
+x_110 = !lean_is_exclusive(x_8);
+if (x_110 == 0)
 {
 return x_8;
 }
 else
 {
-lean_object* x_108; lean_object* x_109; lean_object* x_110; 
-x_108 = lean_ctor_get(x_8, 0);
-x_109 = lean_ctor_get(x_8, 1);
-lean_inc(x_109);
-lean_inc(x_108);
+lean_object* x_111; lean_object* x_112; lean_object* x_113; 
+x_111 = lean_ctor_get(x_8, 0);
+x_112 = lean_ctor_get(x_8, 1);
+lean_inc(x_112);
+lean_inc(x_111);
 lean_dec(x_8);
-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;
+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;
 }
 }
 }
@@ -1384,6 +1391,7 @@ lean_object* initialize_Lean_Compiler_IR_UnboxResult(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_ElimDeadBranches(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_EmitC(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_CtorLayout(lean_object*);
+lean_object* initialize_Lean_Compiler_IR_Sorry(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Lean_Compiler_IR(lean_object* w) {
 lean_object * res;
@@ -1443,6 +1451,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Compiler_IR_CtorLayout(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Compiler_IR_Sorry(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__1 = _init_l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__1();
 lean_mark_persistent(l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__1);
 l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__2 = _init_l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__2();
diff --git a/stage0/stdlib/Lean/Compiler/IR/CompilerM.c b/stage0/stdlib/Lean/Compiler/IR/CompilerM.c
index f476411914..a0e97c47cf 100644
--- a/stage0/stdlib/Lean/Compiler/IR/CompilerM.c
+++ b/stage0/stdlib/Lean/Compiler/IR/CompilerM.c
@@ -79,6 +79,7 @@ lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__2(lean
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____spec__6(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Log_format___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_getSorryDep_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Std_PersistentHashMap_insertAux___rarg___closed__3;
 lean_object* l_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____closed__4;
 uint8_t l_Lean_SMap_contains___at_Lean_IR_containsDecl___spec__1(lean_object*, lean_object*);
@@ -183,6 +184,7 @@ lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_IR_findEnvDecl___spec__2
 lean_object* l_Lean_IR_tracePrefixOptionName___closed__1;
 lean_object* l_Std_HashMapImp_find_x3f___at_Lean_IR_findEnvDecl___spec__5(lean_object*, lean_object*);
 lean_object* l_Lean_IR_findEnvDecl_x27___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_getSorryDep_match__1(lean_object*);
 lean_object* l_Lean_IR_getDecl_match__1(lean_object*);
 lean_object* l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_addDecl(lean_object*, lean_object*, lean_object*);
@@ -196,6 +198,7 @@ extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2;
 lean_object* l_Lean_IR_modifyEnv___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_ir_find_env_decl(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_decl_get_sorry_dep(lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_insert___at_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_findAux___at_Lean_IR_findEnvDecl___spec__3(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____lambda__2___boxed(lean_object*);
@@ -4004,6 +4007,98 @@ lean_dec(x_2);
 return x_5;
 }
 }
+lean_object* l_Lean_IR_getSorryDep_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; 
+lean_dec(x_2);
+x_4 = lean_apply_1(x_3, x_1);
+return x_4;
+}
+else
+{
+lean_object* x_5; 
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_5, 1);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_5, 2);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_5, 3);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_5, 4);
+lean_inc(x_10);
+lean_dec(x_5);
+x_11 = lean_apply_5(x_2, x_6, x_7, x_8, x_9, x_10);
+return x_11;
+}
+else
+{
+lean_object* x_12; 
+lean_dec(x_5);
+lean_dec(x_2);
+x_12 = lean_apply_1(x_3, x_1);
+return x_12;
+}
+}
+}
+}
+lean_object* l_Lean_IR_getSorryDep_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_getSorryDep_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* lean_decl_get_sorry_dep(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_3 = l_Lean_IR_declMapExt;
+x_4 = l_Lean_SimplePersistentEnvExtension_getState___rarg(x_3, x_1);
+lean_dec(x_1);
+x_5 = l_Lean_SMap_find_x3f___at_Lean_IR_findEnvDecl___spec__1(x_4, x_2);
+lean_dec(x_2);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; 
+x_6 = lean_box(0);
+return x_6;
+}
+else
+{
+lean_object* x_7; 
+x_7 = lean_ctor_get(x_5, 0);
+lean_inc(x_7);
+lean_dec(x_5);
+if (lean_obj_tag(x_7) == 0)
+{
+lean_object* x_8; 
+x_8 = lean_ctor_get(x_7, 4);
+lean_inc(x_8);
+lean_dec(x_7);
+return x_8;
+}
+else
+{
+lean_object* x_9; 
+lean_dec(x_7);
+x_9 = lean_box(0);
+return x_9;
+}
+}
+}
+}
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Environment(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_Basic(lean_object*);
diff --git a/stage0/stdlib/Lean/Compiler/IR/Sorry.c b/stage0/stdlib/Lean/Compiler/IR/Sorry.c
new file mode 100644
index 0000000000..a4a84795f5
--- /dev/null
+++ b/stage0/stdlib/Lean/Compiler/IR/Sorry.c
@@ -0,0 +1,2199 @@
+// Lean compiler output
+// Module: Lean.Compiler.IR.Sorry
+// Imports: Init Lean.Compiler.IR.CompilerM
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+size_t l_USize_add(size_t, size_t);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__1;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
+uint8_t l_USize_decEq(size_t, size_t);
+lean_object* lean_array_uget(lean_object*, size_t);
+lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_visitFndBody___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t lean_name_eq(lean_object*, lean_object*);
+lean_object* l_Lean_IR_updateSorryDep_match__3___rarg(lean_object*, lean_object*);
+lean_object* lean_array_get_size(lean_object*);
+extern lean_object* l_Lean_Compiler_checkIsDefinition___closed__3;
+lean_object* l_Lean_IR_Sorry_visitDecl_match__3___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__1___rarg(lean_object*, lean_object*);
+uint8_t l_USize_decLt(size_t, size_t);
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__1(lean_object*);
+lean_object* l_Lean_IR_Sorry_visitDecl(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_updateSorryDep_match__1(lean_object*);
+lean_object* l_Lean_IR_Sorry_visitDecl_match__3(lean_object*);
+lean_object* l_Lean_IR_AltCore_body(lean_object*);
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_visitFndBody___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitFndBody___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__2(lean_object*);
+uint8_t l_Lean_IR_FnBody_isTerminal(lean_object*);
+lean_object* l_Lean_IR_Sorry_State_localSorryMap___default;
+lean_object* l_Lean_IR_updateSorryDep_match__3(lean_object*);
+lean_object* l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_match__1(lean_object*);
+lean_object* l_Lean_IR_Sorry_visitDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_updateSorryDep_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_updateSorryDep___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitFndBody(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_updateSorryDep___spec__1(lean_object*, size_t, size_t, lean_object*);
+lean_object* l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSyntaxAux___spec__2(lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_collect___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_collect___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+size_t lean_usize_of_nat(lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_collect___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitDecl_match__2(lean_object*);
+lean_object* l_Lean_IR_updateSorryDep(lean_object*, lean_object*, lean_object*);
+uint8_t lean_nat_dec_le(lean_object*, lean_object*);
+uint8_t l_Lean_IR_Sorry_State_modified___default;
+lean_object* l_Lean_IR_updateSorryDep___closed__1;
+lean_object* l_Lean_IR_updateSorryDep_match__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_updateSorryDep___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__1(lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__2;
+lean_object* l_Lean_IR_Sorry_visitDecl_match__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__2(lean_object*);
+lean_object* l_Lean_IR_Sorry_visitDecl_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_FnBody_body(lean_object*);
+lean_object* l_Lean_IR_Sorry_collect(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_updateSorryDep_match__2(lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_findDecl(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+lean_object* l_Lean_IR_Sorry_visitDecl_match__1(lean_object*);
+static lean_object* _init_l_Lean_IR_Sorry_State_localSorryMap___default() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+static uint8_t _init_l_Lean_IR_Sorry_State_modified___default() {
+_start:
+{
+uint8_t x_1; 
+x_1 = 0;
+return x_1;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; 
+lean_dec(x_2);
+x_4 = lean_apply_1(x_3, x_1);
+return x_4;
+}
+else
+{
+lean_object* x_5; 
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; 
+x_6 = lean_ctor_get(x_5, 4);
+lean_inc(x_6);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; 
+lean_dec(x_5);
+lean_dec(x_2);
+x_7 = lean_apply_1(x_3, x_1);
+return x_7;
+}
+else
+{
+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_dec(x_3);
+lean_dec(x_1);
+x_8 = lean_ctor_get(x_5, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_5, 1);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_5, 2);
+lean_inc(x_10);
+x_11 = lean_ctor_get(x_5, 3);
+lean_inc(x_11);
+lean_dec(x_5);
+x_12 = lean_ctor_get(x_6, 0);
+lean_inc(x_12);
+lean_dec(x_6);
+x_13 = lean_apply_5(x_2, x_8, x_9, x_10, x_11, x_12);
+return x_13;
+}
+}
+else
+{
+lean_object* x_14; 
+lean_dec(x_5);
+lean_dec(x_2);
+x_14 = lean_apply_1(x_3, x_1);
+return x_14;
+}
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; 
+lean_dec(x_2);
+x_4 = lean_apply_1(x_3, x_1);
+return x_4;
+}
+else
+{
+lean_object* x_5; lean_object* x_6; 
+lean_dec(x_3);
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+lean_dec(x_1);
+x_6 = lean_apply_1(x_2, x_5);
+return x_6;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__2(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f_match__2___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+switch (lean_obj_tag(x_1)) {
+case 6:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+lean_dec(x_4);
+lean_dec(x_3);
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_1, 1);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_2(x_2, x_5, x_6);
+return x_7;
+}
+case 7:
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+lean_dec(x_4);
+lean_dec(x_2);
+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_apply_2(x_3, x_8, x_9);
+return x_10;
+}
+default: 
+{
+lean_object* x_11; 
+lean_dec(x_3);
+lean_dec(x_2);
+x_11 = lean_apply_1(x_4, x_1);
+return x_11;
+}
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitExpr_match__1___rarg), 4, 0);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("sorryAx");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; uint8_t x_6; 
+x_5 = l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__2;
+x_6 = lean_name_eq(x_1, x_5);
+if (x_6 == 0)
+{
+lean_object* x_7; lean_object* x_8; 
+x_7 = lean_ctor_get(x_2, 0);
+lean_inc(x_7);
+x_8 = l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSyntaxAux___spec__2(x_7, x_1);
+lean_dec(x_7);
+if (lean_obj_tag(x_8) == 0)
+{
+lean_object* x_9; lean_object* x_10; 
+lean_inc(x_1);
+x_9 = l_Lean_IR_findDecl(x_1, x_3, x_4);
+x_10 = lean_ctor_get(x_9, 0);
+lean_inc(x_10);
+if (lean_obj_tag(x_10) == 0)
+{
+uint8_t x_11; 
+lean_dec(x_1);
+x_11 = !lean_is_exclusive(x_9);
+if (x_11 == 0)
+{
+lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_12 = lean_ctor_get(x_9, 0);
+lean_dec(x_12);
+x_13 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_14 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_14, 0, x_13);
+lean_ctor_set(x_14, 1, x_2);
+lean_ctor_set(x_9, 0, x_14);
+return x_9;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_15 = lean_ctor_get(x_9, 1);
+lean_inc(x_15);
+lean_dec(x_9);
+x_16 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_17 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_17, 0, x_16);
+lean_ctor_set(x_17, 1, x_2);
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_17);
+lean_ctor_set(x_18, 1, x_15);
+return x_18;
+}
+}
+else
+{
+lean_object* x_19; 
+x_19 = lean_ctor_get(x_10, 0);
+lean_inc(x_19);
+lean_dec(x_10);
+if (lean_obj_tag(x_19) == 0)
+{
+lean_object* x_20; 
+x_20 = lean_ctor_get(x_19, 4);
+lean_inc(x_20);
+lean_dec(x_19);
+if (lean_obj_tag(x_20) == 0)
+{
+uint8_t x_21; 
+lean_dec(x_1);
+x_21 = !lean_is_exclusive(x_9);
+if (x_21 == 0)
+{
+lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_22 = lean_ctor_get(x_9, 0);
+lean_dec(x_22);
+x_23 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_24 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_24, 0, x_23);
+lean_ctor_set(x_24, 1, x_2);
+lean_ctor_set(x_9, 0, x_24);
+return x_9;
+}
+else
+{
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_25 = lean_ctor_get(x_9, 1);
+lean_inc(x_25);
+lean_dec(x_9);
+x_26 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_27 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_27, 0, x_26);
+lean_ctor_set(x_27, 1, x_2);
+x_28 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_28, 0, x_27);
+lean_ctor_set(x_28, 1, x_25);
+return x_28;
+}
+}
+else
+{
+uint8_t x_29; 
+x_29 = !lean_is_exclusive(x_9);
+if (x_29 == 0)
+{
+lean_object* x_30; lean_object* x_31; uint8_t x_32; 
+x_30 = lean_ctor_get(x_9, 0);
+lean_dec(x_30);
+x_31 = lean_ctor_get(x_20, 0);
+lean_inc(x_31);
+lean_dec(x_20);
+x_32 = lean_name_eq(x_31, x_5);
+if (x_32 == 0)
+{
+lean_object* x_33; lean_object* x_34; 
+lean_dec(x_1);
+x_33 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_33, 0, x_31);
+x_34 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_34, 0, x_33);
+lean_ctor_set(x_34, 1, x_2);
+lean_ctor_set(x_9, 0, x_34);
+return x_9;
+}
+else
+{
+lean_object* x_35; lean_object* x_36; 
+lean_dec(x_31);
+x_35 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_35, 0, x_1);
+x_36 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_36, 0, x_35);
+lean_ctor_set(x_36, 1, x_2);
+lean_ctor_set(x_9, 0, x_36);
+return x_9;
+}
+}
+else
+{
+lean_object* x_37; lean_object* x_38; uint8_t x_39; 
+x_37 = lean_ctor_get(x_9, 1);
+lean_inc(x_37);
+lean_dec(x_9);
+x_38 = lean_ctor_get(x_20, 0);
+lean_inc(x_38);
+lean_dec(x_20);
+x_39 = lean_name_eq(x_38, x_5);
+if (x_39 == 0)
+{
+lean_object* x_40; lean_object* x_41; lean_object* x_42; 
+lean_dec(x_1);
+x_40 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_40, 0, x_38);
+x_41 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_41, 0, x_40);
+lean_ctor_set(x_41, 1, x_2);
+x_42 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_42, 0, x_41);
+lean_ctor_set(x_42, 1, x_37);
+return x_42;
+}
+else
+{
+lean_object* x_43; lean_object* x_44; lean_object* x_45; 
+lean_dec(x_38);
+x_43 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_43, 0, x_1);
+x_44 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_44, 0, x_43);
+lean_ctor_set(x_44, 1, x_2);
+x_45 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_45, 0, x_44);
+lean_ctor_set(x_45, 1, x_37);
+return x_45;
+}
+}
+}
+}
+else
+{
+uint8_t x_46; 
+lean_dec(x_19);
+lean_dec(x_1);
+x_46 = !lean_is_exclusive(x_9);
+if (x_46 == 0)
+{
+lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_47 = lean_ctor_get(x_9, 0);
+lean_dec(x_47);
+x_48 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_49 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_49, 0, x_48);
+lean_ctor_set(x_49, 1, x_2);
+lean_ctor_set(x_9, 0, x_49);
+return x_9;
+}
+else
+{
+lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; 
+x_50 = lean_ctor_get(x_9, 1);
+lean_inc(x_50);
+lean_dec(x_9);
+x_51 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_52 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_52, 0, x_51);
+lean_ctor_set(x_52, 1, x_2);
+x_53 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_53, 0, x_52);
+lean_ctor_set(x_53, 1, x_50);
+return x_53;
+}
+}
+}
+}
+else
+{
+lean_object* x_54; uint8_t x_55; 
+x_54 = lean_ctor_get(x_8, 0);
+lean_inc(x_54);
+lean_dec(x_8);
+x_55 = lean_name_eq(x_54, x_5);
+if (x_55 == 0)
+{
+lean_object* x_56; lean_object* x_57; lean_object* x_58; 
+lean_dec(x_1);
+x_56 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_56, 0, x_54);
+x_57 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_57, 0, x_56);
+lean_ctor_set(x_57, 1, x_2);
+x_58 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_58, 0, x_57);
+lean_ctor_set(x_58, 1, x_4);
+return x_58;
+}
+else
+{
+lean_object* x_59; lean_object* x_60; lean_object* x_61; 
+lean_dec(x_54);
+x_59 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_59, 0, x_1);
+x_60 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_60, 0, x_59);
+lean_ctor_set(x_60, 1, x_2);
+x_61 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_61, 0, x_60);
+lean_ctor_set(x_61, 1, x_4);
+return x_61;
+}
+}
+}
+else
+{
+lean_object* x_62; lean_object* x_63; lean_object* x_64; 
+x_62 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_62, 0, x_1);
+x_63 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_63, 0, x_62);
+lean_ctor_set(x_63, 1, x_2);
+x_64 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_64, 0, x_63);
+lean_ctor_set(x_64, 1, x_4);
+return x_64;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+switch (lean_obj_tag(x_1)) {
+case 6:
+{
+lean_object* x_5; lean_object* x_6; 
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+lean_dec(x_1);
+x_6 = l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f(x_5, x_2, x_3, x_4);
+return x_6;
+}
+case 7:
+{
+lean_object* x_7; lean_object* x_8; 
+x_7 = lean_ctor_get(x_1, 0);
+lean_inc(x_7);
+lean_dec(x_1);
+x_8 = l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f(x_7, x_2, x_3, x_4);
+return x_8;
+}
+default: 
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+lean_dec(x_1);
+x_9 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_2);
+x_11 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_11, 0, x_10);
+lean_ctor_set(x_11, 1, x_4);
+return x_11;
+}
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitExpr___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_IR_Sorry_visitExpr(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__1___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+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_apply_2(x_2, x_3, x_4);
+return x_5;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitFndBody_match__1___rarg), 2, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+switch (lean_obj_tag(x_1)) {
+case 0:
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_1, 1);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_1, 2);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_1, 3);
+lean_inc(x_9);
+lean_dec(x_1);
+x_10 = lean_apply_4(x_2, x_6, x_7, x_8, x_9);
+return x_10;
+}
+case 1:
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_2);
+x_11 = lean_ctor_get(x_1, 0);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_1, 1);
+lean_inc(x_12);
+x_13 = lean_ctor_get(x_1, 2);
+lean_inc(x_13);
+x_14 = lean_ctor_get(x_1, 3);
+lean_inc(x_14);
+lean_dec(x_1);
+x_15 = lean_apply_4(x_3, x_11, x_12, x_13, x_14);
+return x_15;
+}
+case 10:
+{
+lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_2);
+x_16 = lean_ctor_get(x_1, 0);
+lean_inc(x_16);
+x_17 = lean_ctor_get(x_1, 1);
+lean_inc(x_17);
+x_18 = lean_ctor_get(x_1, 2);
+lean_inc(x_18);
+x_19 = lean_ctor_get(x_1, 3);
+lean_inc(x_19);
+lean_dec(x_1);
+x_20 = lean_apply_4(x_4, x_16, x_17, x_18, x_19);
+return x_20;
+}
+default: 
+{
+lean_object* x_21; 
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_21 = lean_apply_1(x_5, x_1);
+return x_21;
+}
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitFndBody_match__2(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitFndBody_match__2___rarg), 5, 0);
+return x_2;
+}
+}
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_visitFndBody___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) {
+_start:
+{
+uint8_t x_8; 
+x_8 = x_2 == x_3;
+if (x_8 == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+lean_dec(x_4);
+x_9 = lean_array_uget(x_1, x_2);
+x_10 = l_Lean_IR_AltCore_body(x_9);
+lean_dec(x_9);
+x_11 = l_Lean_IR_Sorry_visitFndBody(x_10, x_5, x_6, x_7);
+x_12 = lean_ctor_get(x_11, 0);
+lean_inc(x_12);
+x_13 = lean_ctor_get(x_12, 0);
+lean_inc(x_13);
+if (lean_obj_tag(x_13) == 0)
+{
+uint8_t x_14; 
+x_14 = !lean_is_exclusive(x_11);
+if (x_14 == 0)
+{
+lean_object* x_15; uint8_t x_16; 
+x_15 = lean_ctor_get(x_11, 0);
+lean_dec(x_15);
+x_16 = !lean_is_exclusive(x_12);
+if (x_16 == 0)
+{
+lean_object* x_17; uint8_t x_18; 
+x_17 = lean_ctor_get(x_12, 0);
+lean_dec(x_17);
+x_18 = !lean_is_exclusive(x_13);
+if (x_18 == 0)
+{
+return x_11;
+}
+else
+{
+lean_object* x_19; lean_object* x_20; 
+x_19 = lean_ctor_get(x_13, 0);
+lean_inc(x_19);
+lean_dec(x_13);
+x_20 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_20, 0, x_19);
+lean_ctor_set(x_12, 0, x_20);
+return x_11;
+}
+}
+else
+{
+lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_21 = lean_ctor_get(x_12, 1);
+lean_inc(x_21);
+lean_dec(x_12);
+x_22 = lean_ctor_get(x_13, 0);
+lean_inc(x_22);
+if (lean_is_exclusive(x_13)) {
+ lean_ctor_release(x_13, 0);
+ x_23 = x_13;
+} else {
+ lean_dec_ref(x_13);
+ x_23 = lean_box(0);
+}
+if (lean_is_scalar(x_23)) {
+ x_24 = lean_alloc_ctor(0, 1, 0);
+} else {
+ x_24 = x_23;
+}
+lean_ctor_set(x_24, 0, x_22);
+x_25 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_25, 0, x_24);
+lean_ctor_set(x_25, 1, x_21);
+lean_ctor_set(x_11, 0, x_25);
+return x_11;
+}
+}
+else
+{
+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_26 = lean_ctor_get(x_11, 1);
+lean_inc(x_26);
+lean_dec(x_11);
+x_27 = lean_ctor_get(x_12, 1);
+lean_inc(x_27);
+if (lean_is_exclusive(x_12)) {
+ lean_ctor_release(x_12, 0);
+ lean_ctor_release(x_12, 1);
+ x_28 = x_12;
+} else {
+ lean_dec_ref(x_12);
+ x_28 = lean_box(0);
+}
+x_29 = lean_ctor_get(x_13, 0);
+lean_inc(x_29);
+if (lean_is_exclusive(x_13)) {
+ lean_ctor_release(x_13, 0);
+ x_30 = x_13;
+} else {
+ lean_dec_ref(x_13);
+ x_30 = lean_box(0);
+}
+if (lean_is_scalar(x_30)) {
+ x_31 = lean_alloc_ctor(0, 1, 0);
+} else {
+ x_31 = x_30;
+}
+lean_ctor_set(x_31, 0, x_29);
+if (lean_is_scalar(x_28)) {
+ x_32 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_32 = x_28;
+}
+lean_ctor_set(x_32, 0, x_31);
+lean_ctor_set(x_32, 1, x_27);
+x_33 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_33, 0, x_32);
+lean_ctor_set(x_33, 1, x_26);
+return x_33;
+}
+}
+else
+{
+lean_object* x_34; lean_object* x_35; lean_object* x_36; size_t x_37; size_t x_38; 
+x_34 = lean_ctor_get(x_11, 1);
+lean_inc(x_34);
+lean_dec(x_11);
+x_35 = lean_ctor_get(x_12, 1);
+lean_inc(x_35);
+lean_dec(x_12);
+x_36 = lean_ctor_get(x_13, 0);
+lean_inc(x_36);
+lean_dec(x_13);
+x_37 = 1;
+x_38 = x_2 + x_37;
+x_2 = x_38;
+x_4 = x_36;
+x_5 = x_35;
+x_7 = x_34;
+goto _start;
+}
+}
+else
+{
+lean_object* x_40; lean_object* x_41; lean_object* x_42; 
+x_40 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_40, 0, x_4);
+x_41 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_41, 0, x_40);
+lean_ctor_set(x_41, 1, x_5);
+x_42 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_42, 0, x_41);
+lean_ctor_set(x_42, 1, x_7);
+return x_42;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitFndBody(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+switch (lean_obj_tag(x_1)) {
+case 0:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_5 = lean_ctor_get(x_1, 2);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_1, 3);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = l_Lean_IR_Sorry_visitExpr(x_5, x_2, x_3, x_4);
+x_8 = lean_ctor_get(x_7, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_8, 0);
+lean_inc(x_9);
+if (lean_obj_tag(x_9) == 0)
+{
+uint8_t x_10; 
+lean_dec(x_6);
+x_10 = !lean_is_exclusive(x_7);
+if (x_10 == 0)
+{
+lean_object* x_11; uint8_t x_12; 
+x_11 = lean_ctor_get(x_7, 0);
+lean_dec(x_11);
+x_12 = !lean_is_exclusive(x_8);
+if (x_12 == 0)
+{
+lean_object* x_13; uint8_t x_14; 
+x_13 = lean_ctor_get(x_8, 0);
+lean_dec(x_13);
+x_14 = !lean_is_exclusive(x_9);
+if (x_14 == 0)
+{
+return x_7;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; 
+x_15 = lean_ctor_get(x_9, 0);
+lean_inc(x_15);
+lean_dec(x_9);
+x_16 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_16, 0, x_15);
+lean_ctor_set(x_8, 0, x_16);
+return x_7;
+}
+}
+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_8, 1);
+lean_inc(x_17);
+lean_dec(x_8);
+x_18 = lean_ctor_get(x_9, 0);
+lean_inc(x_18);
+if (lean_is_exclusive(x_9)) {
+ lean_ctor_release(x_9, 0);
+ x_19 = x_9;
+} else {
+ lean_dec_ref(x_9);
+ x_19 = lean_box(0);
+}
+if (lean_is_scalar(x_19)) {
+ x_20 = lean_alloc_ctor(0, 1, 0);
+} else {
+ x_20 = x_19;
+}
+lean_ctor_set(x_20, 0, x_18);
+x_21 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_21, 0, x_20);
+lean_ctor_set(x_21, 1, x_17);
+lean_ctor_set(x_7, 0, x_21);
+return x_7;
+}
+}
+else
+{
+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; 
+x_22 = lean_ctor_get(x_7, 1);
+lean_inc(x_22);
+lean_dec(x_7);
+x_23 = lean_ctor_get(x_8, 1);
+lean_inc(x_23);
+if (lean_is_exclusive(x_8)) {
+ lean_ctor_release(x_8, 0);
+ lean_ctor_release(x_8, 1);
+ x_24 = x_8;
+} else {
+ lean_dec_ref(x_8);
+ x_24 = lean_box(0);
+}
+x_25 = lean_ctor_get(x_9, 0);
+lean_inc(x_25);
+if (lean_is_exclusive(x_9)) {
+ lean_ctor_release(x_9, 0);
+ x_26 = x_9;
+} else {
+ lean_dec_ref(x_9);
+ x_26 = lean_box(0);
+}
+if (lean_is_scalar(x_26)) {
+ x_27 = lean_alloc_ctor(0, 1, 0);
+} else {
+ x_27 = x_26;
+}
+lean_ctor_set(x_27, 0, x_25);
+if (lean_is_scalar(x_24)) {
+ x_28 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_28 = x_24;
+}
+lean_ctor_set(x_28, 0, x_27);
+lean_ctor_set(x_28, 1, x_23);
+x_29 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_29, 0, x_28);
+lean_ctor_set(x_29, 1, x_22);
+return x_29;
+}
+}
+else
+{
+lean_object* x_30; lean_object* x_31; 
+lean_dec(x_9);
+x_30 = lean_ctor_get(x_7, 1);
+lean_inc(x_30);
+lean_dec(x_7);
+x_31 = lean_ctor_get(x_8, 1);
+lean_inc(x_31);
+lean_dec(x_8);
+x_1 = x_6;
+x_2 = x_31;
+x_4 = x_30;
+goto _start;
+}
+}
+case 1:
+{
+lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; 
+x_33 = lean_ctor_get(x_1, 2);
+lean_inc(x_33);
+x_34 = lean_ctor_get(x_1, 3);
+lean_inc(x_34);
+lean_dec(x_1);
+x_35 = l_Lean_IR_Sorry_visitFndBody(x_33, x_2, x_3, x_4);
+x_36 = lean_ctor_get(x_35, 0);
+lean_inc(x_36);
+x_37 = lean_ctor_get(x_36, 0);
+lean_inc(x_37);
+if (lean_obj_tag(x_37) == 0)
+{
+uint8_t x_38; 
+lean_dec(x_34);
+x_38 = !lean_is_exclusive(x_35);
+if (x_38 == 0)
+{
+lean_object* x_39; uint8_t x_40; 
+x_39 = lean_ctor_get(x_35, 0);
+lean_dec(x_39);
+x_40 = !lean_is_exclusive(x_36);
+if (x_40 == 0)
+{
+lean_object* x_41; uint8_t x_42; 
+x_41 = lean_ctor_get(x_36, 0);
+lean_dec(x_41);
+x_42 = !lean_is_exclusive(x_37);
+if (x_42 == 0)
+{
+return x_35;
+}
+else
+{
+lean_object* x_43; lean_object* x_44; 
+x_43 = lean_ctor_get(x_37, 0);
+lean_inc(x_43);
+lean_dec(x_37);
+x_44 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_44, 0, x_43);
+lean_ctor_set(x_36, 0, x_44);
+return x_35;
+}
+}
+else
+{
+lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_45 = lean_ctor_get(x_36, 1);
+lean_inc(x_45);
+lean_dec(x_36);
+x_46 = lean_ctor_get(x_37, 0);
+lean_inc(x_46);
+if (lean_is_exclusive(x_37)) {
+ lean_ctor_release(x_37, 0);
+ x_47 = x_37;
+} else {
+ lean_dec_ref(x_37);
+ x_47 = lean_box(0);
+}
+if (lean_is_scalar(x_47)) {
+ x_48 = lean_alloc_ctor(0, 1, 0);
+} else {
+ x_48 = x_47;
+}
+lean_ctor_set(x_48, 0, x_46);
+x_49 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_49, 0, x_48);
+lean_ctor_set(x_49, 1, x_45);
+lean_ctor_set(x_35, 0, x_49);
+return x_35;
+}
+}
+else
+{
+lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; 
+x_50 = lean_ctor_get(x_35, 1);
+lean_inc(x_50);
+lean_dec(x_35);
+x_51 = lean_ctor_get(x_36, 1);
+lean_inc(x_51);
+if (lean_is_exclusive(x_36)) {
+ lean_ctor_release(x_36, 0);
+ lean_ctor_release(x_36, 1);
+ x_52 = x_36;
+} else {
+ lean_dec_ref(x_36);
+ x_52 = lean_box(0);
+}
+x_53 = lean_ctor_get(x_37, 0);
+lean_inc(x_53);
+if (lean_is_exclusive(x_37)) {
+ lean_ctor_release(x_37, 0);
+ x_54 = x_37;
+} else {
+ lean_dec_ref(x_37);
+ x_54 = lean_box(0);
+}
+if (lean_is_scalar(x_54)) {
+ x_55 = lean_alloc_ctor(0, 1, 0);
+} else {
+ x_55 = x_54;
+}
+lean_ctor_set(x_55, 0, x_53);
+if (lean_is_scalar(x_52)) {
+ x_56 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_56 = x_52;
+}
+lean_ctor_set(x_56, 0, x_55);
+lean_ctor_set(x_56, 1, x_51);
+x_57 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_57, 0, x_56);
+lean_ctor_set(x_57, 1, x_50);
+return x_57;
+}
+}
+else
+{
+lean_object* x_58; lean_object* x_59; 
+lean_dec(x_37);
+x_58 = lean_ctor_get(x_35, 1);
+lean_inc(x_58);
+lean_dec(x_35);
+x_59 = lean_ctor_get(x_36, 1);
+lean_inc(x_59);
+lean_dec(x_36);
+x_1 = x_34;
+x_2 = x_59;
+x_4 = x_58;
+goto _start;
+}
+}
+case 10:
+{
+lean_object* x_61; lean_object* x_62; lean_object* x_63; uint8_t x_64; 
+x_61 = lean_ctor_get(x_1, 3);
+lean_inc(x_61);
+lean_dec(x_1);
+x_62 = lean_array_get_size(x_61);
+x_63 = lean_unsigned_to_nat(0u);
+x_64 = lean_nat_dec_lt(x_63, x_62);
+if (x_64 == 0)
+{
+lean_object* x_65; lean_object* x_66; lean_object* x_67; 
+lean_dec(x_62);
+lean_dec(x_61);
+x_65 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_66 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_66, 0, x_65);
+lean_ctor_set(x_66, 1, x_2);
+x_67 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_67, 0, x_66);
+lean_ctor_set(x_67, 1, x_4);
+return x_67;
+}
+else
+{
+uint8_t x_68; 
+x_68 = lean_nat_dec_le(x_62, x_62);
+if (x_68 == 0)
+{
+lean_object* x_69; lean_object* x_70; lean_object* x_71; 
+lean_dec(x_62);
+lean_dec(x_61);
+x_69 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_70 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_70, 0, x_69);
+lean_ctor_set(x_70, 1, x_2);
+x_71 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_71, 0, x_70);
+lean_ctor_set(x_71, 1, x_4);
+return x_71;
+}
+else
+{
+size_t x_72; size_t x_73; lean_object* x_74; lean_object* x_75; 
+x_72 = 0;
+x_73 = lean_usize_of_nat(x_62);
+lean_dec(x_62);
+x_74 = lean_box(0);
+x_75 = l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_visitFndBody___spec__1(x_61, x_72, x_73, x_74, x_2, x_3, x_4);
+lean_dec(x_61);
+return x_75;
+}
+}
+}
+default: 
+{
+uint8_t x_76; 
+x_76 = l_Lean_IR_FnBody_isTerminal(x_1);
+if (x_76 == 0)
+{
+lean_object* x_77; 
+x_77 = l_Lean_IR_FnBody_body(x_1);
+lean_dec(x_1);
+x_1 = x_77;
+goto _start;
+}
+else
+{
+lean_object* x_79; lean_object* x_80; lean_object* x_81; 
+lean_dec(x_1);
+x_79 = l_Lean_Compiler_checkIsDefinition___closed__3;
+x_80 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_80, 0, x_79);
+lean_ctor_set(x_80, 1, x_2);
+x_81 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_81, 0, x_80);
+lean_ctor_set(x_81, 1, x_4);
+return x_81;
+}
+}
+}
+}
+}
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_visitFndBody___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) {
+_start:
+{
+size_t x_8; size_t x_9; lean_object* x_10; 
+x_8 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_9 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_10 = l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_visitFndBody___spec__1(x_1, x_8, x_9, x_4, x_5, x_6, x_7);
+lean_dec(x_6);
+lean_dec(x_1);
+return x_10;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitFndBody___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_IR_Sorry_visitFndBody(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_2);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_apply_1(x_3, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_2, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitDecl_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_2);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_3, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_2, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl_match__2(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitDecl_match__2___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl_match__3___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 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_dec(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+x_5 = lean_ctor_get(x_1, 1);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_1, 2);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_1, 3);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_1, 4);
+lean_inc(x_8);
+lean_dec(x_1);
+x_9 = lean_apply_5(x_2, x_4, x_5, x_6, x_7, x_8);
+return x_9;
+}
+else
+{
+lean_object* x_10; 
+lean_dec(x_2);
+x_10 = lean_apply_1(x_3, x_1);
+return x_10;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl_match__3(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_Sorry_visitDecl_match__3___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_1, 3);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_ctor_get(x_2, 0);
+lean_inc(x_7);
+x_8 = l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSyntaxAux___spec__2(x_7, x_5);
+lean_dec(x_7);
+if (lean_obj_tag(x_8) == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_9 = l_Lean_IR_Sorry_visitFndBody(x_6, x_2, x_3, x_4);
+x_10 = lean_ctor_get(x_9, 0);
+lean_inc(x_10);
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
+if (lean_obj_tag(x_11) == 0)
+{
+uint8_t x_12; 
+x_12 = !lean_is_exclusive(x_9);
+if (x_12 == 0)
+{
+lean_object* x_13; uint8_t x_14; 
+x_13 = lean_ctor_get(x_9, 0);
+lean_dec(x_13);
+x_14 = !lean_is_exclusive(x_10);
+if (x_14 == 0)
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; 
+x_15 = lean_ctor_get(x_10, 1);
+x_16 = lean_ctor_get(x_10, 0);
+lean_dec(x_16);
+x_17 = lean_ctor_get(x_11, 0);
+lean_inc(x_17);
+lean_dec(x_11);
+x_18 = lean_ctor_get(x_15, 0);
+lean_inc(x_18);
+lean_dec(x_15);
+x_19 = l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_18, x_5, x_17);
+x_20 = 1;
+x_21 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_21, 0, x_19);
+lean_ctor_set_uint8(x_21, sizeof(void*)*1, x_20);
+x_22 = lean_box(0);
+lean_ctor_set(x_10, 1, x_21);
+lean_ctor_set(x_10, 0, x_22);
+return x_9;
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
+x_23 = lean_ctor_get(x_10, 1);
+lean_inc(x_23);
+lean_dec(x_10);
+x_24 = lean_ctor_get(x_11, 0);
+lean_inc(x_24);
+lean_dec(x_11);
+x_25 = lean_ctor_get(x_23, 0);
+lean_inc(x_25);
+lean_dec(x_23);
+x_26 = l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_25, x_5, x_24);
+x_27 = 1;
+x_28 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_28, 0, x_26);
+lean_ctor_set_uint8(x_28, sizeof(void*)*1, x_27);
+x_29 = lean_box(0);
+x_30 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_30, 0, x_29);
+lean_ctor_set(x_30, 1, x_28);
+lean_ctor_set(x_9, 0, x_30);
+return x_9;
+}
+}
+else
+{
+lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; 
+x_31 = lean_ctor_get(x_9, 1);
+lean_inc(x_31);
+lean_dec(x_9);
+x_32 = lean_ctor_get(x_10, 1);
+lean_inc(x_32);
+if (lean_is_exclusive(x_10)) {
+ lean_ctor_release(x_10, 0);
+ lean_ctor_release(x_10, 1);
+ x_33 = x_10;
+} else {
+ lean_dec_ref(x_10);
+ x_33 = lean_box(0);
+}
+x_34 = lean_ctor_get(x_11, 0);
+lean_inc(x_34);
+lean_dec(x_11);
+x_35 = lean_ctor_get(x_32, 0);
+lean_inc(x_35);
+lean_dec(x_32);
+x_36 = l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_35, x_5, x_34);
+x_37 = 1;
+x_38 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_38, 0, x_36);
+lean_ctor_set_uint8(x_38, sizeof(void*)*1, x_37);
+x_39 = lean_box(0);
+if (lean_is_scalar(x_33)) {
+ x_40 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_40 = x_33;
+}
+lean_ctor_set(x_40, 0, x_39);
+lean_ctor_set(x_40, 1, x_38);
+x_41 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_41, 0, x_40);
+lean_ctor_set(x_41, 1, x_31);
+return x_41;
+}
+}
+else
+{
+uint8_t x_42; 
+lean_dec(x_11);
+lean_dec(x_5);
+x_42 = !lean_is_exclusive(x_9);
+if (x_42 == 0)
+{
+lean_object* x_43; uint8_t x_44; 
+x_43 = lean_ctor_get(x_9, 0);
+lean_dec(x_43);
+x_44 = !lean_is_exclusive(x_10);
+if (x_44 == 0)
+{
+lean_object* x_45; lean_object* x_46; 
+x_45 = lean_ctor_get(x_10, 0);
+lean_dec(x_45);
+x_46 = lean_box(0);
+lean_ctor_set(x_10, 0, x_46);
+return x_9;
+}
+else
+{
+lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_47 = lean_ctor_get(x_10, 1);
+lean_inc(x_47);
+lean_dec(x_10);
+x_48 = lean_box(0);
+x_49 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_49, 0, x_48);
+lean_ctor_set(x_49, 1, x_47);
+lean_ctor_set(x_9, 0, x_49);
+return x_9;
+}
+}
+else
+{
+lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_50 = lean_ctor_get(x_9, 1);
+lean_inc(x_50);
+lean_dec(x_9);
+x_51 = lean_ctor_get(x_10, 1);
+lean_inc(x_51);
+if (lean_is_exclusive(x_10)) {
+ lean_ctor_release(x_10, 0);
+ lean_ctor_release(x_10, 1);
+ x_52 = x_10;
+} else {
+ lean_dec_ref(x_10);
+ x_52 = lean_box(0);
+}
+x_53 = lean_box(0);
+if (lean_is_scalar(x_52)) {
+ x_54 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_54 = x_52;
+}
+lean_ctor_set(x_54, 0, x_53);
+lean_ctor_set(x_54, 1, x_51);
+x_55 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_55, 0, x_54);
+lean_ctor_set(x_55, 1, x_50);
+return x_55;
+}
+}
+}
+else
+{
+lean_object* x_56; lean_object* x_57; lean_object* x_58; 
+lean_dec(x_8);
+lean_dec(x_6);
+lean_dec(x_5);
+x_56 = lean_box(0);
+x_57 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_57, 0, x_56);
+lean_ctor_set(x_57, 1, x_2);
+x_58 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_58, 0, x_57);
+lean_ctor_set(x_58, 1, x_4);
+return x_58;
+}
+}
+else
+{
+lean_object* x_59; lean_object* x_60; lean_object* x_61; 
+lean_dec(x_1);
+x_59 = lean_box(0);
+x_60 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_60, 0, x_59);
+lean_ctor_set(x_60, 1, x_2);
+x_61 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_61, 0, x_60);
+lean_ctor_set(x_61, 1, x_4);
+return x_61;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_visitDecl___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_IR_Sorry_visitDecl(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_collect___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) {
+_start:
+{
+uint8_t x_8; 
+x_8 = x_2 == x_3;
+if (x_8 == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; 
+lean_dec(x_4);
+x_9 = lean_array_uget(x_1, x_2);
+x_10 = l_Lean_IR_Sorry_visitDecl(x_9, x_5, x_6, x_7);
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_10, 1);
+lean_inc(x_12);
+lean_dec(x_10);
+x_13 = lean_ctor_get(x_11, 0);
+lean_inc(x_13);
+x_14 = lean_ctor_get(x_11, 1);
+lean_inc(x_14);
+lean_dec(x_11);
+x_15 = 1;
+x_16 = x_2 + x_15;
+x_2 = x_16;
+x_4 = x_13;
+x_5 = x_14;
+x_7 = x_12;
+goto _start;
+}
+else
+{
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_4);
+lean_ctor_set(x_18, 1, x_5);
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_18);
+lean_ctor_set(x_19, 1, x_7);
+return x_19;
+}
+}
+}
+lean_object* l_Lean_IR_Sorry_collect(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+uint8_t x_5; 
+x_5 = !lean_is_exclusive(x_2);
+if (x_5 == 0)
+{
+uint8_t x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; 
+x_6 = 0;
+lean_ctor_set_uint8(x_2, sizeof(void*)*1, x_6);
+x_7 = lean_array_get_size(x_1);
+x_8 = lean_unsigned_to_nat(0u);
+x_9 = lean_nat_dec_lt(x_8, x_7);
+if (x_9 == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_dec(x_7);
+x_10 = lean_box(0);
+x_11 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_11, 0, x_10);
+lean_ctor_set(x_11, 1, x_2);
+x_12 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_12, 0, x_11);
+lean_ctor_set(x_12, 1, x_4);
+return x_12;
+}
+else
+{
+uint8_t x_13; 
+x_13 = lean_nat_dec_le(x_7, x_7);
+if (x_13 == 0)
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+lean_dec(x_7);
+x_14 = lean_box(0);
+x_15 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_15, 0, x_14);
+lean_ctor_set(x_15, 1, x_2);
+x_16 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_16, 0, x_15);
+lean_ctor_set(x_16, 1, x_4);
+return x_16;
+}
+else
+{
+size_t x_17; size_t x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; 
+x_17 = 0;
+x_18 = lean_usize_of_nat(x_7);
+lean_dec(x_7);
+x_19 = lean_box(0);
+x_20 = l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_collect___spec__1(x_1, x_17, x_18, x_19, x_2, x_3, x_4);
+x_21 = lean_ctor_get(x_20, 0);
+lean_inc(x_21);
+x_22 = !lean_is_exclusive(x_21);
+if (x_22 == 0)
+{
+lean_object* x_23; lean_object* x_24; uint8_t x_25; 
+x_23 = lean_ctor_get(x_21, 1);
+x_24 = lean_ctor_get(x_21, 0);
+lean_dec(x_24);
+x_25 = lean_ctor_get_uint8(x_23, sizeof(void*)*1);
+if (x_25 == 0)
+{
+uint8_t x_26; 
+x_26 = !lean_is_exclusive(x_20);
+if (x_26 == 0)
+{
+lean_object* x_27; 
+x_27 = lean_ctor_get(x_20, 0);
+lean_dec(x_27);
+lean_ctor_set(x_21, 0, x_19);
+return x_20;
+}
+else
+{
+lean_object* x_28; lean_object* x_29; 
+x_28 = lean_ctor_get(x_20, 1);
+lean_inc(x_28);
+lean_dec(x_20);
+lean_ctor_set(x_21, 0, x_19);
+x_29 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_29, 0, x_21);
+lean_ctor_set(x_29, 1, x_28);
+return x_29;
+}
+}
+else
+{
+lean_object* x_30; 
+lean_free_object(x_21);
+x_30 = lean_ctor_get(x_20, 1);
+lean_inc(x_30);
+lean_dec(x_20);
+x_2 = x_23;
+x_4 = x_30;
+goto _start;
+}
+}
+else
+{
+lean_object* x_32; uint8_t x_33; 
+x_32 = lean_ctor_get(x_21, 1);
+lean_inc(x_32);
+lean_dec(x_21);
+x_33 = lean_ctor_get_uint8(x_32, sizeof(void*)*1);
+if (x_33 == 0)
+{
+lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; 
+x_34 = lean_ctor_get(x_20, 1);
+lean_inc(x_34);
+if (lean_is_exclusive(x_20)) {
+ lean_ctor_release(x_20, 0);
+ lean_ctor_release(x_20, 1);
+ x_35 = x_20;
+} else {
+ lean_dec_ref(x_20);
+ x_35 = lean_box(0);
+}
+x_36 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_36, 0, x_19);
+lean_ctor_set(x_36, 1, x_32);
+if (lean_is_scalar(x_35)) {
+ x_37 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_37 = x_35;
+}
+lean_ctor_set(x_37, 0, x_36);
+lean_ctor_set(x_37, 1, x_34);
+return x_37;
+}
+else
+{
+lean_object* x_38; 
+x_38 = lean_ctor_get(x_20, 1);
+lean_inc(x_38);
+lean_dec(x_20);
+x_2 = x_32;
+x_4 = x_38;
+goto _start;
+}
+}
+}
+}
+}
+else
+{
+lean_object* x_40; uint8_t x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45; 
+x_40 = lean_ctor_get(x_2, 0);
+lean_inc(x_40);
+lean_dec(x_2);
+x_41 = 0;
+x_42 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_42, 0, x_40);
+lean_ctor_set_uint8(x_42, sizeof(void*)*1, x_41);
+x_43 = lean_array_get_size(x_1);
+x_44 = lean_unsigned_to_nat(0u);
+x_45 = lean_nat_dec_lt(x_44, x_43);
+if (x_45 == 0)
+{
+lean_object* x_46; lean_object* x_47; lean_object* x_48; 
+lean_dec(x_43);
+x_46 = lean_box(0);
+x_47 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_47, 0, x_46);
+lean_ctor_set(x_47, 1, x_42);
+x_48 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_48, 0, x_47);
+lean_ctor_set(x_48, 1, x_4);
+return x_48;
+}
+else
+{
+uint8_t x_49; 
+x_49 = lean_nat_dec_le(x_43, x_43);
+if (x_49 == 0)
+{
+lean_object* x_50; lean_object* x_51; lean_object* x_52; 
+lean_dec(x_43);
+x_50 = lean_box(0);
+x_51 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_51, 0, x_50);
+lean_ctor_set(x_51, 1, x_42);
+x_52 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_52, 0, x_51);
+lean_ctor_set(x_52, 1, x_4);
+return x_52;
+}
+else
+{
+size_t x_53; size_t x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; uint8_t x_60; 
+x_53 = 0;
+x_54 = lean_usize_of_nat(x_43);
+lean_dec(x_43);
+x_55 = lean_box(0);
+x_56 = l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_collect___spec__1(x_1, x_53, x_54, x_55, x_42, x_3, x_4);
+x_57 = lean_ctor_get(x_56, 0);
+lean_inc(x_57);
+x_58 = lean_ctor_get(x_57, 1);
+lean_inc(x_58);
+if (lean_is_exclusive(x_57)) {
+ lean_ctor_release(x_57, 0);
+ lean_ctor_release(x_57, 1);
+ x_59 = x_57;
+} else {
+ lean_dec_ref(x_57);
+ x_59 = lean_box(0);
+}
+x_60 = lean_ctor_get_uint8(x_58, sizeof(void*)*1);
+if (x_60 == 0)
+{
+lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; 
+x_61 = lean_ctor_get(x_56, 1);
+lean_inc(x_61);
+if (lean_is_exclusive(x_56)) {
+ lean_ctor_release(x_56, 0);
+ lean_ctor_release(x_56, 1);
+ x_62 = x_56;
+} else {
+ lean_dec_ref(x_56);
+ x_62 = lean_box(0);
+}
+if (lean_is_scalar(x_59)) {
+ x_63 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_63 = x_59;
+}
+lean_ctor_set(x_63, 0, x_55);
+lean_ctor_set(x_63, 1, x_58);
+if (lean_is_scalar(x_62)) {
+ x_64 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_64 = x_62;
+}
+lean_ctor_set(x_64, 0, x_63);
+lean_ctor_set(x_64, 1, x_61);
+return x_64;
+}
+else
+{
+lean_object* x_65; 
+lean_dec(x_59);
+x_65 = lean_ctor_get(x_56, 1);
+lean_inc(x_65);
+lean_dec(x_56);
+x_2 = x_58;
+x_4 = x_65;
+goto _start;
+}
+}
+}
+}
+}
+}
+lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_collect___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) {
+_start:
+{
+size_t x_8; size_t x_9; lean_object* x_10; 
+x_8 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_9 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_10 = l_Array_foldlMUnsafe_fold___at_Lean_IR_Sorry_collect___spec__1(x_1, x_8, x_9, x_4, x_5, x_6, x_7);
+lean_dec(x_6);
+lean_dec(x_1);
+return x_10;
+}
+}
+lean_object* l_Lean_IR_Sorry_collect___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_IR_Sorry_collect(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_5;
+}
+}
+lean_object* l_Lean_IR_updateSorryDep_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; 
+lean_dec(x_2);
+x_4 = lean_apply_1(x_3, x_1);
+return x_4;
+}
+else
+{
+lean_object* x_5; lean_object* x_6; 
+lean_dec(x_3);
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+lean_dec(x_1);
+x_6 = lean_apply_1(x_2, x_5);
+return x_6;
+}
+}
+}
+lean_object* l_Lean_IR_updateSorryDep_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_updateSorryDep_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_updateSorryDep_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 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_dec(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+x_5 = lean_ctor_get(x_1, 1);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_1, 2);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_1, 3);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_1, 4);
+lean_inc(x_8);
+lean_dec(x_1);
+x_9 = lean_apply_5(x_2, x_4, x_5, x_6, x_7, x_8);
+return x_9;
+}
+else
+{
+lean_object* x_10; 
+lean_dec(x_2);
+x_10 = lean_apply_1(x_3, x_1);
+return x_10;
+}
+}
+}
+lean_object* l_Lean_IR_updateSorryDep_match__2(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_updateSorryDep_match__2___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_IR_updateSorryDep_match__3___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+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_apply_2(x_2, x_3, x_4);
+return x_5;
+}
+}
+lean_object* l_Lean_IR_updateSorryDep_match__3(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_updateSorryDep_match__3___rarg), 2, 0);
+return x_2;
+}
+}
+lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_updateSorryDep___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 = x_3 < x_2;
+if (x_5 == 0)
+{
+lean_object* x_6; 
+x_6 = x_4;
+return x_6;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; 
+x_7 = lean_array_uget(x_4, x_3);
+x_8 = lean_unsigned_to_nat(0u);
+x_9 = lean_array_uset(x_4, x_3, x_8);
+x_10 = x_7;
+x_11 = 1;
+x_12 = x_3 + x_11;
+if (lean_obj_tag(x_10) == 0)
+{
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_13 = lean_ctor_get(x_10, 0);
+lean_inc(x_13);
+x_14 = lean_ctor_get(x_10, 1);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_10, 2);
+lean_inc(x_15);
+x_16 = lean_ctor_get(x_10, 3);
+lean_inc(x_16);
+x_17 = lean_ctor_get(x_1, 0);
+x_18 = l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSyntaxAux___spec__2(x_17, x_13);
+if (lean_obj_tag(x_18) == 0)
+{
+lean_object* x_19; lean_object* x_20; 
+lean_dec(x_16);
+lean_dec(x_15);
+lean_dec(x_14);
+lean_dec(x_13);
+x_19 = x_10;
+x_20 = lean_array_uset(x_9, x_3, x_19);
+x_3 = x_12;
+x_4 = x_20;
+goto _start;
+}
+else
+{
+uint8_t x_22; 
+x_22 = !lean_is_exclusive(x_10);
+if (x_22 == 0)
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; 
+x_23 = lean_ctor_get(x_10, 4);
+lean_dec(x_23);
+x_24 = lean_ctor_get(x_10, 3);
+lean_dec(x_24);
+x_25 = lean_ctor_get(x_10, 2);
+lean_dec(x_25);
+x_26 = lean_ctor_get(x_10, 1);
+lean_dec(x_26);
+x_27 = lean_ctor_get(x_10, 0);
+lean_dec(x_27);
+x_28 = !lean_is_exclusive(x_18);
+if (x_28 == 0)
+{
+lean_object* x_29; lean_object* x_30; 
+lean_ctor_set(x_10, 4, x_18);
+x_29 = x_10;
+x_30 = lean_array_uset(x_9, x_3, x_29);
+x_3 = x_12;
+x_4 = x_30;
+goto _start;
+}
+else
+{
+lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+x_32 = lean_ctor_get(x_18, 0);
+lean_inc(x_32);
+lean_dec(x_18);
+x_33 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_33, 0, x_32);
+lean_ctor_set(x_10, 4, x_33);
+x_34 = x_10;
+x_35 = lean_array_uset(x_9, x_3, x_34);
+x_3 = x_12;
+x_4 = x_35;
+goto _start;
+}
+}
+else
+{
+lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; 
+lean_dec(x_10);
+x_37 = lean_ctor_get(x_18, 0);
+lean_inc(x_37);
+if (lean_is_exclusive(x_18)) {
+ lean_ctor_release(x_18, 0);
+ x_38 = x_18;
+} else {
+ lean_dec_ref(x_18);
+ x_38 = lean_box(0);
+}
+if (lean_is_scalar(x_38)) {
+ x_39 = lean_alloc_ctor(1, 1, 0);
+} else {
+ x_39 = x_38;
+}
+lean_ctor_set(x_39, 0, x_37);
+x_40 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_40, 0, x_13);
+lean_ctor_set(x_40, 1, x_14);
+lean_ctor_set(x_40, 2, x_15);
+lean_ctor_set(x_40, 3, x_16);
+lean_ctor_set(x_40, 4, x_39);
+x_41 = x_40;
+x_42 = lean_array_uset(x_9, x_3, x_41);
+x_3 = x_12;
+x_4 = x_42;
+goto _start;
+}
+}
+}
+else
+{
+lean_object* x_44; lean_object* x_45; 
+x_44 = x_10;
+x_45 = lean_array_uset(x_9, x_3, x_44);
+x_3 = x_12;
+x_4 = x_45;
+goto _start;
+}
+}
+}
+}
+static lean_object* _init_l_Lean_IR_updateSorryDep___closed__1() {
+_start:
+{
+lean_object* x_1; uint8_t x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = 0;
+x_3 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_IR_updateSorryDep(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; uint8_t x_6; 
+x_4 = l_Lean_IR_updateSorryDep___closed__1;
+x_5 = l_Lean_IR_Sorry_collect(x_1, x_4, x_2, x_3);
+x_6 = !lean_is_exclusive(x_5);
+if (x_6 == 0)
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; size_t x_10; size_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_7 = lean_ctor_get(x_5, 0);
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = lean_array_get_size(x_1);
+x_10 = lean_usize_of_nat(x_9);
+lean_dec(x_9);
+x_11 = 0;
+x_12 = x_1;
+x_13 = l_Array_mapMUnsafe_map___at_Lean_IR_updateSorryDep___spec__1(x_8, x_10, x_11, x_12);
+lean_dec(x_8);
+x_14 = x_13;
+lean_ctor_set(x_5, 0, x_14);
+return x_5;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; size_t x_19; size_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_15 = lean_ctor_get(x_5, 0);
+x_16 = lean_ctor_get(x_5, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_5);
+x_17 = lean_ctor_get(x_15, 1);
+lean_inc(x_17);
+lean_dec(x_15);
+x_18 = lean_array_get_size(x_1);
+x_19 = lean_usize_of_nat(x_18);
+lean_dec(x_18);
+x_20 = 0;
+x_21 = x_1;
+x_22 = l_Array_mapMUnsafe_map___at_Lean_IR_updateSorryDep___spec__1(x_17, x_19, x_20, x_21);
+lean_dec(x_17);
+x_23 = x_22;
+x_24 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_24, 0, x_23);
+lean_ctor_set(x_24, 1, x_16);
+return x_24;
+}
+}
+}
+lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_updateSorryDep___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_mapMUnsafe_map___at_Lean_IR_updateSorryDep___spec__1(x_1, x_5, x_6, x_4);
+lean_dec(x_1);
+return x_7;
+}
+}
+lean_object* l_Lean_IR_updateSorryDep___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_IR_updateSorryDep(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
+lean_object* initialize_Init(lean_object*);
+lean_object* initialize_Lean_Compiler_IR_CompilerM(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Lean_Compiler_IR_Sorry(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = initialize_Init(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Compiler_IR_CompilerM(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_IR_Sorry_State_localSorryMap___default = _init_l_Lean_IR_Sorry_State_localSorryMap___default();
+lean_mark_persistent(l_Lean_IR_Sorry_State_localSorryMap___default);
+l_Lean_IR_Sorry_State_modified___default = _init_l_Lean_IR_Sorry_State_modified___default();
+l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__1 = _init_l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__1();
+lean_mark_persistent(l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__1);
+l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__2 = _init_l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__2();
+lean_mark_persistent(l_Lean_IR_Sorry_visitExpr_getSorryDepFor_x3f___closed__2);
+l_Lean_IR_updateSorryDep___closed__1 = _init_l_Lean_IR_updateSorryDep___closed__1();
+lean_mark_persistent(l_Lean_IR_updateSorryDep___closed__1);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif