chore: update stage0

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

@@ -163,7 +163,7 @@ else do
     x fvars
 
 @[inline] def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α :=
-elabBinders #[binder] (fun fvars => x (fvars.get! 1))
+elabBinders #[binder] (fun fvars => x (fvars.get! 0))
 
 @[builtinTermElab «forall»] def elabForall : TermElab :=
 fun stx _ => match_syntax stx with

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

@@ -22,7 +22,7 @@ withMVarContext mvarId $ fun ctx s =>
 
 def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do
 val ← instantiateMVars ref (mkMVar mvarId);
-when val.hasMVar $ throwError ref ("tactic failed, result still contain metavariables" ++ indentExpr val)
+when val.hasExprMVar $ throwError ref ("tactic failed, result still contain metavariables" ++ indentExpr val)
 
 def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
 modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };

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

@@ -9,3 +9,4 @@ import Init.Lean.Elab.Tactic.Basic
 import Init.Lean.Elab.Tactic.ElabTerm
 import Init.Lean.Elab.Tactic.Induction
 import Init.Lean.Elab.Tactic.Generalize
+import Init.Lean.Elab.Tactic.Injection

stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Meta.Tactic.Apply
+import Init.Lean.Meta.Tactic.Assert
 import Init.Lean.Elab.Tactic.Basic
 import Init.Lean.Elab.SyntheticMVars
 
@@ -68,6 +69,29 @@ fun stx => match_syntax stx with
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 
+/--
+  Elaborate `stx`. If it a free variable, return it. Otherwise, assert it, and return the free variable.
+  Note that, the main goal is updated when `Meta.assert` is used in the second case. -/
+def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId := do
+(mvarId, others) ← getMainGoal stx;
+withMVarContext mvarId $ do
+  e ← elabTerm stx none;
+  match e with
+  | Expr.fvar fvarId _ => pure fvarId
+  | _ => do
+    type ← inferType stx e;
+    let intro (userName : Name) (useUnusedNames : Bool) : TacticM FVarId := do {
+      (fvarId, mvarId) ← liftMetaM stx $ do {
+        mvarId ← Meta.assert mvarId userName type e;
+        Meta.intro1 mvarId useUnusedNames
+      };
+      setGoals $ mvarId::others;
+      pure fvarId
+    };
+    match userName? with
+    | none          => intro `h true
+    | some userName => intro userName false
+
 end Tactic
 end Elab
 end Lean

stage0/src/Init/Lean/Elab/Tactic/Injection.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.Tactic.Injection
+import Init.Lean.Elab.Tactic.ElabTerm
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+-- optional (" with " >> many1 ident')
+private def getInjectionNewIds (stx : Syntax) : List Name :=
+if stx.isNone then []
+else (stx.getArg 1).getArgs.toList.map Syntax.getId
+
+@[builtinTactic «injection»] def evalInjection : Tactic :=
+fun stx => do
+  -- parser! nonReservedSymbol "injection " >> termParser >> withIds
+  fvarId ← elabAsFVar (stx.getArg 1);
+  let ids := getInjectionNewIds (stx.getArg 2);
+  liftMetaTactic stx $ fun mvarId => do
+    r ← Meta.injection mvarId fvarId ids (!ids.isEmpty);
+    match r with
+    | Meta.InjectionResult.solved             => pure []
+    | Meta.InjectionResult.subgoal mvarId _ _ => pure [mvarId]
+
+end Tactic
+end Elab
+end Lean

stage0/src/Init/Lean/Meta/Tactic/Injection.lean

@@ -54,7 +54,7 @@ withMVarContext mvarId $ do
           newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
           assignExprMVar mvarId (mkApp val newMVar);
           mvarId ← tryClear newMVar.mvarId! fvarId;
-          pure $ InjectionResultCore.subgoal newMVar.mvarId! aCtor.nfields
+          pure $ InjectionResultCore.subgoal mvarId aCtor.nfields
         | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
     | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"
 

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

@@ -124,6 +124,7 @@ def letPatDecl  : Parser := node `Lean.Parser.Term.letDecl $ try (termParser >>
 def letEqnsDecl : Parser := node `Lean.Parser.Term.letDecl $ letIdLhs >> matchAlts false
 def letDecl              := letIdDecl <|> letPatDecl <|> letEqnsDecl
 @[builtinTermParser] def «let» := parser! symbol "let " leadPrec >> letDecl >> "; " >> termParser
+@[builtinTermParser] def «let!» := parser! symbol "let! " leadPrec >> letDecl >> "; " >> termParser
 
 def leftArrow : Parser := unicodeSymbol " ← " " <- "
 def doLet  := parser! "let " >> letDecl

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

@@ -5051,7 +5051,7 @@ _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
 x_5 = l_Lean_Expr_Inhabited;
-x_6 = lean_unsigned_to_nat(1u);
+x_6 = lean_unsigned_to_nat(0u);
 x_7 = lean_array_get(x_5, x_2, x_6);
 x_8 = lean_apply_3(x_1, x_7, x_3, x_4);
 return x_8;

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

@@ -60,6 +60,7 @@ lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVa
 lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_List_forM___main___at___private_Init_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__4;
+uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
 lean_object* l___private_Init_Lean_Elab_SyntheticMVars_6__synthesizeSyntheticMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_lift___at_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*);
@@ -110,7 +111,6 @@ lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SyntheticMVa
 uint8_t l_Lean_Expr_isMVar(lean_object*);
 lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__7;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__9;
-uint8_t l_Lean_Expr_hasMVar(lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SyntheticMVars_4__synthesizePendingCoeInstMVar___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_log___at_Lean_Elab_Term_logTrace___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
@@ -830,7 +830,7 @@ if (x_7 == 0)
 lean_object* x_8; lean_object* x_9; uint8_t x_10; 
 x_8 = lean_ctor_get(x_6, 0);
 x_9 = lean_ctor_get(x_6, 1);
-x_10 = l_Lean_Expr_hasMVar(x_8);
+x_10 = l_Lean_Expr_hasExprMVar(x_8);
 if (x_10 == 0)
 {
 lean_object* x_11; 
@@ -863,7 +863,7 @@ x_18 = lean_ctor_get(x_6, 1);
 lean_inc(x_18);
 lean_inc(x_17);
 lean_dec(x_6);
-x_19 = l_Lean_Expr_hasMVar(x_17);
+x_19 = l_Lean_Expr_hasExprMVar(x_17);
 if (x_19 == 0)
 {
 lean_object* x_20; lean_object* x_21; 

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

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab.Tactic
-// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction Init.Lean.Elab.Tactic.Generalize
+// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction Init.Lean.Elab.Tactic.Generalize Init.Lean.Elab.Tactic.Injection
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -18,6 +18,7 @@ lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_Induction(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_Generalize(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Tactic_Injection(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab_Tactic(lean_object* w) {
 lean_object * res;
@@ -38,6 +39,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_Tactic_Generalize(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Tactic_Injection(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab.Tactic.ElabTerm
-// Imports: Init.Lean.Meta.Tactic.Apply Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.SyntheticMVars
+// Imports: Init.Lean.Meta.Tactic.Apply Init.Lean.Meta.Tactic.Assert Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.SyntheticMVars
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -13,15 +13,20 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__1;
 lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__2;
+lean_object* l_Lean_Meta_assert___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1;
 lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalApply(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_inferType(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalRefine(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact(lean_object*);
 lean_object* l___private_Init_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux___main(uint8_t, lean_object*, lean_object*, lean_object*);
@@ -33,18 +38,23 @@ extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
 lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_apply___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine(lean_object*);
 lean_object* l_Lean_Elab_Tactic_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalRefine___lambda__1___closed__1;
 lean_object* l_Lean_Elab_Tactic_elabTerm___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1;
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1;
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2;
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2;
 lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1___closed__1;
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
@@ -52,15 +62,19 @@ lean_object* l_Lean_Elab_Tactic_evalRefine___lambda__1(lean_object*, lean_object
 lean_object* l_Lean_Elab_Tactic_setGoals(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_ensureHasNoMVars(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3;
 lean_object* l_Lean_Elab_Tactic_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
+lean_object* l_Lean_Meta_intro1(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_collectMVars(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__3;
@@ -1309,7 +1323,385 @@ x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint8_t x_4; lean_object* x_5; 
+x_4 = 1;
+x_5 = l_Lean_Meta_intro1(x_1, x_4, x_2, x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint8_t x_4; lean_object* x_5; 
+x_4 = 0;
+x_5 = l_Lean_Meta_intro1(x_1, x_4, x_2, x_3);
+return x_5;
+}
+}
+lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("h");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabAsFVar___lambda__1___boxed), 3, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabAsFVar___lambda__2___boxed), 3, 0);
+return x_1;
+}
+}
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; 
+if (lean_obj_tag(x_5) == 1)
+{
+lean_object* x_57; lean_object* x_58; 
+lean_dec(x_6);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+x_57 = lean_ctor_get(x_5, 0);
+lean_inc(x_57);
+lean_dec(x_5);
+x_58 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_58, 0, x_57);
+lean_ctor_set(x_58, 1, x_7);
+return x_58;
+}
+else
+{
+lean_object* x_59; 
+x_59 = lean_box(0);
+x_8 = x_59;
+goto block_56;
+}
+block_56:
+{
+lean_object* x_9; 
+lean_dec(x_8);
+lean_inc(x_6);
+lean_inc(x_5);
+lean_inc(x_1);
+x_9 = l_Lean_Elab_Tactic_inferType(x_1, x_5, x_6, x_7);
+if (lean_obj_tag(x_9) == 0)
+{
+if (lean_obj_tag(x_2) == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_10 = lean_ctor_get(x_9, 0);
+lean_inc(x_10);
+x_11 = lean_ctor_get(x_9, 1);
+lean_inc(x_11);
+lean_dec(x_9);
+x_12 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2;
+x_13 = lean_alloc_closure((void*)(l_Lean_Meta_assert___boxed), 6, 4);
+lean_closure_set(x_13, 0, x_3);
+lean_closure_set(x_13, 1, x_12);
+lean_closure_set(x_13, 2, x_10);
+lean_closure_set(x_13, 3, x_5);
+x_14 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3;
+x_15 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2);
+lean_closure_set(x_15, 0, x_13);
+lean_closure_set(x_15, 1, x_14);
+lean_inc(x_6);
+x_16 = l_Lean_Elab_Tactic_liftMetaM___rarg(x_1, x_15, x_6, x_11);
+if (lean_obj_tag(x_16) == 0)
+{
+lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; 
+x_17 = lean_ctor_get(x_16, 0);
+lean_inc(x_17);
+x_18 = lean_ctor_get(x_16, 1);
+lean_inc(x_18);
+lean_dec(x_16);
+x_19 = lean_ctor_get(x_17, 0);
+lean_inc(x_19);
+x_20 = lean_ctor_get(x_17, 1);
+lean_inc(x_20);
+lean_dec(x_17);
+x_21 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_21, 0, x_20);
+lean_ctor_set(x_21, 1, x_4);
+x_22 = l_Lean_Elab_Tactic_setGoals(x_21, x_6, x_18);
+lean_dec(x_6);
+x_23 = !lean_is_exclusive(x_22);
+if (x_23 == 0)
+{
+lean_object* x_24; 
+x_24 = lean_ctor_get(x_22, 0);
+lean_dec(x_24);
+lean_ctor_set(x_22, 0, x_19);
+return x_22;
+}
+else
+{
+lean_object* x_25; lean_object* x_26; 
+x_25 = lean_ctor_get(x_22, 1);
+lean_inc(x_25);
+lean_dec(x_22);
+x_26 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_26, 0, x_19);
+lean_ctor_set(x_26, 1, x_25);
+return x_26;
+}
+}
+else
+{
+uint8_t x_27; 
+lean_dec(x_6);
+lean_dec(x_4);
+x_27 = !lean_is_exclusive(x_16);
+if (x_27 == 0)
+{
+return x_16;
+}
+else
+{
+lean_object* x_28; lean_object* x_29; lean_object* x_30; 
+x_28 = lean_ctor_get(x_16, 0);
+x_29 = lean_ctor_get(x_16, 1);
+lean_inc(x_29);
+lean_inc(x_28);
+lean_dec(x_16);
+x_30 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_30, 0, x_28);
+lean_ctor_set(x_30, 1, x_29);
+return x_30;
+}
+}
+}
+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; lean_object* x_37; 
+x_31 = lean_ctor_get(x_9, 0);
+lean_inc(x_31);
+x_32 = lean_ctor_get(x_9, 1);
+lean_inc(x_32);
+lean_dec(x_9);
+x_33 = lean_ctor_get(x_2, 0);
+lean_inc(x_33);
+lean_dec(x_2);
+x_34 = lean_alloc_closure((void*)(l_Lean_Meta_assert___boxed), 6, 4);
+lean_closure_set(x_34, 0, x_3);
+lean_closure_set(x_34, 1, x_33);
+lean_closure_set(x_34, 2, x_31);
+lean_closure_set(x_34, 3, x_5);
+x_35 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4;
+x_36 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2);
+lean_closure_set(x_36, 0, x_34);
+lean_closure_set(x_36, 1, x_35);
+lean_inc(x_6);
+x_37 = l_Lean_Elab_Tactic_liftMetaM___rarg(x_1, x_36, x_6, x_32);
+if (lean_obj_tag(x_37) == 0)
+{
+lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; 
+x_38 = lean_ctor_get(x_37, 0);
+lean_inc(x_38);
+x_39 = lean_ctor_get(x_37, 1);
+lean_inc(x_39);
+lean_dec(x_37);
+x_40 = lean_ctor_get(x_38, 0);
+lean_inc(x_40);
+x_41 = lean_ctor_get(x_38, 1);
+lean_inc(x_41);
+lean_dec(x_38);
+x_42 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_42, 0, x_41);
+lean_ctor_set(x_42, 1, x_4);
+x_43 = l_Lean_Elab_Tactic_setGoals(x_42, x_6, x_39);
+lean_dec(x_6);
+x_44 = !lean_is_exclusive(x_43);
+if (x_44 == 0)
+{
+lean_object* x_45; 
+x_45 = lean_ctor_get(x_43, 0);
+lean_dec(x_45);
+lean_ctor_set(x_43, 0, x_40);
+return x_43;
+}
+else
+{
+lean_object* x_46; lean_object* x_47; 
+x_46 = lean_ctor_get(x_43, 1);
+lean_inc(x_46);
+lean_dec(x_43);
+x_47 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_47, 0, x_40);
+lean_ctor_set(x_47, 1, x_46);
+return x_47;
+}
+}
+else
+{
+uint8_t x_48; 
+lean_dec(x_6);
+lean_dec(x_4);
+x_48 = !lean_is_exclusive(x_37);
+if (x_48 == 0)
+{
+return x_37;
+}
+else
+{
+lean_object* x_49; lean_object* x_50; lean_object* x_51; 
+x_49 = lean_ctor_get(x_37, 0);
+x_50 = lean_ctor_get(x_37, 1);
+lean_inc(x_50);
+lean_inc(x_49);
+lean_dec(x_37);
+x_51 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_51, 0, x_49);
+lean_ctor_set(x_51, 1, x_50);
+return x_51;
+}
+}
+}
+}
+else
+{
+uint8_t x_52; 
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+x_52 = !lean_is_exclusive(x_9);
+if (x_52 == 0)
+{
+return x_9;
+}
+else
+{
+lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_53 = lean_ctor_get(x_9, 0);
+x_54 = lean_ctor_get(x_9, 1);
+lean_inc(x_54);
+lean_inc(x_53);
+lean_dec(x_9);
+x_55 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_55, 0, x_53);
+lean_ctor_set(x_55, 1, x_54);
+return x_55;
+}
+}
+}
+}
+}
+lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+lean_inc(x_3);
+lean_inc(x_1);
+x_5 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_3, x_4);
+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; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_5, 1);
+lean_inc(x_7);
+lean_dec(x_5);
+x_8 = lean_ctor_get(x_6, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_6, 1);
+lean_inc(x_9);
+lean_dec(x_6);
+x_10 = lean_box(0);
+x_11 = 0;
+x_12 = lean_box(x_11);
+lean_inc(x_1);
+x_13 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabTerm___boxed), 5, 3);
+lean_closure_set(x_13, 0, x_1);
+lean_closure_set(x_13, 1, x_10);
+lean_closure_set(x_13, 2, x_12);
+lean_inc(x_8);
+x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabAsFVar___lambda__3), 7, 4);
+lean_closure_set(x_14, 0, x_1);
+lean_closure_set(x_14, 1, x_2);
+lean_closure_set(x_14, 2, x_8);
+lean_closure_set(x_14, 3, x_9);
+x_15 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
+lean_closure_set(x_15, 0, x_13);
+lean_closure_set(x_15, 1, x_14);
+x_16 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_8, x_15, x_3, x_7);
+lean_dec(x_8);
+return x_16;
+}
+else
+{
+uint8_t x_17; 
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+x_17 = !lean_is_exclusive(x_5);
+if (x_17 == 0)
+{
+return x_5;
+}
+else
+{
+lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+x_18 = lean_ctor_get(x_5, 0);
+x_19 = lean_ctor_get(x_5, 1);
+lean_inc(x_19);
+lean_inc(x_18);
+lean_dec(x_5);
+x_20 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_20, 0, x_18);
+lean_ctor_set(x_20, 1, x_19);
+return x_20;
+}
+}
+}
+}
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Elab_Tactic_elabAsFVar___lambda__1(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
+lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Elab_Tactic_elabAsFVar___lambda__2(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
 lean_object* initialize_Init_Lean_Meta_Tactic_Apply(lean_object*);
+lean_object* initialize_Init_Lean_Meta_Tactic_Assert(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*);
 lean_object* initialize_Init_Lean_Elab_SyntheticMVars(lean_object*);
 static bool _G_initialized = false;
@@ -1320,6 +1712,9 @@ _G_initialized = true;
 res = initialize_Init_Lean_Meta_Tactic_Apply(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Meta_Tactic_Assert(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_Tactic_Basic(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -1357,6 +1752,14 @@ lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__3
 res = l___regBuiltinTactic_Lean_Elab_Tactic_evalApply(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1();
+lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1);
+l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2();
+lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2);
+l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3();
+lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3);
+l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4();
+lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Init/Lean/Elab/Tactic/Injection.c

@@ -0,0 +1,387 @@
+// Lean compiler output
+// Module: Init.Lean.Elab.Tactic.Injection
+// Imports: Init.Lean.Meta.Tactic.Injection Init.Lean.Elab.Tactic.ElabTerm
+#include "runtime/lean.h"
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Elab_Tactic_liftMetaTactic___closed__1;
+lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1;
+extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
+lean_object* l_Lean_Syntax_getId(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjection___closed__1;
+lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(lean_object*);
+lean_object* l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(lean_object*);
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection(lean_object*);
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2;
+lean_object* l_Lean_Meta_injection___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjection(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_getArgs(lean_object*);
+lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_Lean_Syntax_isNone(lean_object*);
+lean_object* l_Array_toList___rarg(lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
+uint8_t l_List_isEmpty___rarg(lean_object*);
+lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___boxed(lean_object*);
+extern lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__2;
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3;
+lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(lean_object* x_1) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_2; 
+x_2 = lean_box(0);
+return x_2;
+}
+else
+{
+uint8_t x_3; 
+x_3 = !lean_is_exclusive(x_1);
+if (x_3 == 0)
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_ctor_get(x_1, 0);
+x_5 = lean_ctor_get(x_1, 1);
+x_6 = l_Lean_Syntax_getId(x_4);
+lean_dec(x_4);
+x_7 = l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(x_5);
+lean_ctor_set(x_1, 1, x_7);
+lean_ctor_set(x_1, 0, x_6);
+return x_1;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_8 = lean_ctor_get(x_1, 0);
+x_9 = lean_ctor_get(x_1, 1);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_dec(x_1);
+x_10 = l_Lean_Syntax_getId(x_8);
+lean_dec(x_8);
+x_11 = l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(x_9);
+x_12 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_12, 0, x_10);
+lean_ctor_set(x_12, 1, x_11);
+return x_12;
+}
+}
+}
+}
+lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; 
+x_2 = l_Lean_Syntax_isNone(x_1);
+if (x_2 == 0)
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_3 = lean_unsigned_to_nat(1u);
+x_4 = l_Lean_Syntax_getArg(x_1, x_3);
+x_5 = l_Lean_Syntax_getArgs(x_4);
+lean_dec(x_4);
+x_6 = l_Array_toList___rarg(x_5);
+lean_dec(x_5);
+x_7 = l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(x_6);
+return x_7;
+}
+else
+{
+lean_object* x_8; 
+x_8 = lean_box(0);
+return x_8;
+}
+}
+}
+lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1(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; 
+x_4 = lean_box(0);
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_4);
+lean_ctor_set(x_5, 1, x_3);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_6 = lean_ctor_get(x_1, 0);
+x_7 = lean_box(0);
+lean_inc(x_6);
+x_8 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_8, 0, x_6);
+lean_ctor_set(x_8, 1, x_7);
+x_9 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_9, 0, x_8);
+lean_ctor_set(x_9, 1, x_3);
+return x_9;
+}
+}
+}
+lean_object* _init_l_Lean_Elab_Tactic_evalInjection___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjection___lambda__1___boxed), 3, 0);
+return x_1;
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjection(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_unsigned_to_nat(1u);
+x_5 = l_Lean_Syntax_getArg(x_1, x_4);
+x_6 = lean_box(0);
+lean_inc(x_2);
+x_7 = l_Lean_Elab_Tactic_elabAsFVar(x_5, x_6, x_2, x_3);
+if (lean_obj_tag(x_7) == 0)
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_8 = lean_ctor_get(x_7, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_7, 1);
+lean_inc(x_9);
+lean_dec(x_7);
+x_10 = lean_unsigned_to_nat(2u);
+x_11 = l_Lean_Syntax_getArg(x_1, x_10);
+x_12 = l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(x_11);
+lean_dec(x_11);
+lean_inc(x_2);
+lean_inc(x_1);
+x_13 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_9);
+if (lean_obj_tag(x_13) == 0)
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; 
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
+x_16 = lean_ctor_get(x_14, 0);
+lean_inc(x_16);
+x_17 = lean_ctor_get(x_14, 1);
+lean_inc(x_17);
+lean_dec(x_14);
+x_18 = l_List_isEmpty___rarg(x_12);
+x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed), 4, 1);
+lean_closure_set(x_19, 0, x_17);
+if (x_18 == 0)
+{
+uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+x_20 = 1;
+x_21 = lean_box(x_20);
+lean_inc(x_16);
+x_22 = lean_alloc_closure((void*)(l_Lean_Meta_injection___boxed), 6, 4);
+lean_closure_set(x_22, 0, x_16);
+lean_closure_set(x_22, 1, x_8);
+lean_closure_set(x_22, 2, x_12);
+lean_closure_set(x_22, 3, x_21);
+x_23 = l_Lean_Elab_Tactic_evalInjection___closed__1;
+x_24 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2);
+lean_closure_set(x_24, 0, x_22);
+lean_closure_set(x_24, 1, x_23);
+x_25 = l_Lean_Elab_Tactic_liftMetaTactic___closed__1;
+x_26 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2);
+lean_closure_set(x_26, 0, x_24);
+lean_closure_set(x_26, 1, x_25);
+x_27 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaM___rarg), 4, 2);
+lean_closure_set(x_27, 0, x_1);
+lean_closure_set(x_27, 1, x_26);
+x_28 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
+lean_closure_set(x_28, 0, x_27);
+lean_closure_set(x_28, 1, x_19);
+x_29 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_16, x_28, x_2, x_15);
+lean_dec(x_16);
+return x_29;
+}
+else
+{
+uint8_t x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_30 = 0;
+x_31 = lean_box(x_30);
+lean_inc(x_16);
+x_32 = lean_alloc_closure((void*)(l_Lean_Meta_injection___boxed), 6, 4);
+lean_closure_set(x_32, 0, x_16);
+lean_closure_set(x_32, 1, x_8);
+lean_closure_set(x_32, 2, x_12);
+lean_closure_set(x_32, 3, x_31);
+x_33 = l_Lean_Elab_Tactic_evalInjection___closed__1;
+x_34 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2);
+lean_closure_set(x_34, 0, x_32);
+lean_closure_set(x_34, 1, x_33);
+x_35 = l_Lean_Elab_Tactic_liftMetaTactic___closed__1;
+x_36 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2);
+lean_closure_set(x_36, 0, x_34);
+lean_closure_set(x_36, 1, x_35);
+x_37 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaM___rarg), 4, 2);
+lean_closure_set(x_37, 0, x_1);
+lean_closure_set(x_37, 1, x_36);
+x_38 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
+lean_closure_set(x_38, 0, x_37);
+lean_closure_set(x_38, 1, x_19);
+x_39 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_16, x_38, x_2, x_15);
+lean_dec(x_16);
+return x_39;
+}
+}
+else
+{
+uint8_t x_40; 
+lean_dec(x_12);
+lean_dec(x_8);
+lean_dec(x_2);
+lean_dec(x_1);
+x_40 = !lean_is_exclusive(x_13);
+if (x_40 == 0)
+{
+return x_13;
+}
+else
+{
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_13, 0);
+x_42 = lean_ctor_get(x_13, 1);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_dec(x_13);
+x_43 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_43, 0, x_41);
+lean_ctor_set(x_43, 1, x_42);
+return x_43;
+}
+}
+}
+else
+{
+uint8_t x_44; 
+lean_dec(x_2);
+lean_dec(x_1);
+x_44 = !lean_is_exclusive(x_7);
+if (x_44 == 0)
+{
+return x_7;
+}
+else
+{
+lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_45 = lean_ctor_get(x_7, 0);
+x_46 = lean_ctor_get(x_7, 1);
+lean_inc(x_46);
+lean_inc(x_45);
+lean_dec(x_7);
+x_47 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_47, 0, x_45);
+lean_ctor_set(x_47, 1, x_46);
+return x_47;
+}
+}
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Elab_Tactic_evalInjection___lambda__1(x_1, x_2, x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
+lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("evalInjection");
+return x_1;
+}
+}
+lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
+x_2 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjection), 3, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_Tactic_injection___elambda__1___closed__2;
+x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2;
+x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3;
+x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+lean_object* initialize_Init_Lean_Meta_Tactic_Injection(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_Lean_Elab_Tactic_Injection(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_mk_io_result(lean_box(0));
+_G_initialized = true;
+res = initialize_Init_Lean_Meta_Tactic_Injection(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_Elab_Tactic_evalInjection___closed__1 = _init_l_Lean_Elab_Tactic_evalInjection___closed__1();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalInjection___closed__1);
+l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1();
+lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1);
+l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2();
+lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2);
+l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3();
+lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3);
+res = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_mk_io_result(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif

stage0/stdlib/Init/Lean/Meta/Tactic/Injection.c

@@ -587,7 +587,6 @@ lean_inc(x_89);
 lean_dec(x_88);
 x_90 = l_Lean_Expr_mvarId_x21(x_85);
 lean_dec(x_85);
-lean_inc(x_90);
 x_91 = l_Lean_Meta_tryClear(x_90, x_1, x_5, x_89);
 lean_dec(x_5);
 if (lean_obj_tag(x_91) == 0)
@@ -598,216 +597,216 @@ if (x_92 == 0)
 {
 lean_object* x_93; lean_object* x_94; lean_object* x_95; 
 x_93 = lean_ctor_get(x_91, 0);
-lean_dec(x_93);
 x_94 = lean_ctor_get(x_50, 4);
 lean_inc(x_94);
 lean_dec(x_50);
 x_95 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_95, 0, x_90);
+lean_ctor_set(x_95, 0, x_93);
 lean_ctor_set(x_95, 1, x_94);
 lean_ctor_set(x_91, 0, x_95);
 return x_91;
 }
 else
 {
-lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; 
-x_96 = lean_ctor_get(x_91, 1);
+lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; 
+x_96 = lean_ctor_get(x_91, 0);
+x_97 = lean_ctor_get(x_91, 1);
+lean_inc(x_97);
 lean_inc(x_96);
 lean_dec(x_91);
-x_97 = lean_ctor_get(x_50, 4);
-lean_inc(x_97);
+x_98 = lean_ctor_get(x_50, 4);
+lean_inc(x_98);
 lean_dec(x_50);
-x_98 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_98, 0, x_90);
-lean_ctor_set(x_98, 1, x_97);
-x_99 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_99, 0, x_98);
-lean_ctor_set(x_99, 1, x_96);
-return x_99;
+x_99 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_99, 0, x_96);
+lean_ctor_set(x_99, 1, x_98);
+x_100 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_100, 0, x_99);
+lean_ctor_set(x_100, 1, x_97);
+return x_100;
 }
 }
 else
 {
-uint8_t x_100; 
-lean_dec(x_90);
+uint8_t x_101; 
 lean_dec(x_50);
-x_100 = !lean_is_exclusive(x_91);
-if (x_100 == 0)
+x_101 = !lean_is_exclusive(x_91);
+if (x_101 == 0)
 {
 return x_91;
 }
 else
 {
-lean_object* x_101; lean_object* x_102; lean_object* x_103; 
-x_101 = lean_ctor_get(x_91, 0);
-x_102 = lean_ctor_get(x_91, 1);
+lean_object* x_102; lean_object* x_103; lean_object* x_104; 
+x_102 = lean_ctor_get(x_91, 0);
+x_103 = lean_ctor_get(x_91, 1);
+lean_inc(x_103);
 lean_inc(x_102);
-lean_inc(x_101);
 lean_dec(x_91);
-x_103 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_103, 0, x_101);
-lean_ctor_set(x_103, 1, x_102);
-return x_103;
+x_104 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_104, 0, x_102);
+lean_ctor_set(x_104, 1, x_103);
+return x_104;
 }
 }
 }
 else
 {
-uint8_t x_104; 
+uint8_t x_105; 
 lean_dec(x_85);
 lean_dec(x_50);
 lean_dec(x_5);
 lean_dec(x_1);
-x_104 = !lean_is_exclusive(x_88);
-if (x_104 == 0)
+x_105 = !lean_is_exclusive(x_88);
+if (x_105 == 0)
 {
 return x_88;
 }
 else
 {
-lean_object* x_105; lean_object* x_106; lean_object* x_107; 
-x_105 = lean_ctor_get(x_88, 0);
-x_106 = lean_ctor_get(x_88, 1);
+lean_object* x_106; lean_object* x_107; lean_object* x_108; 
+x_106 = lean_ctor_get(x_88, 0);
+x_107 = lean_ctor_get(x_88, 1);
+lean_inc(x_107);
 lean_inc(x_106);
-lean_inc(x_105);
 lean_dec(x_88);
-x_107 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_107, 0, x_105);
-lean_ctor_set(x_107, 1, x_106);
-return x_107;
+x_108 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_108, 0, x_106);
+lean_ctor_set(x_108, 1, x_107);
+return x_108;
 }
 }
 }
 else
 {
-uint8_t x_108; 
+uint8_t x_109; 
 lean_dec(x_79);
 lean_dec(x_54);
 lean_dec(x_50);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_1);
-x_108 = !lean_is_exclusive(x_80);
-if (x_108 == 0)
+x_109 = !lean_is_exclusive(x_80);
+if (x_109 == 0)
 {
 return x_80;
 }
 else
 {
-lean_object* x_109; lean_object* x_110; lean_object* x_111; 
-x_109 = lean_ctor_get(x_80, 0);
-x_110 = lean_ctor_get(x_80, 1);
+lean_object* x_110; lean_object* x_111; lean_object* x_112; 
+x_110 = lean_ctor_get(x_80, 0);
+x_111 = lean_ctor_get(x_80, 1);
+lean_inc(x_111);
 lean_inc(x_110);
-lean_inc(x_109);
 lean_dec(x_80);
-x_111 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_111, 0, x_109);
-lean_ctor_set(x_111, 1, x_110);
-return x_111;
+x_112 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_112, 0, x_110);
+lean_ctor_set(x_112, 1, x_111);
+return x_112;
 }
 }
 }
 else
 {
-lean_object* x_112; lean_object* x_113; lean_object* x_114; 
+lean_object* x_113; lean_object* x_114; lean_object* x_115; 
 lean_dec(x_76);
 lean_dec(x_54);
 lean_dec(x_50);
 lean_dec(x_1);
-x_112 = lean_ctor_get(x_75, 1);
-lean_inc(x_112);
+x_113 = lean_ctor_get(x_75, 1);
+lean_inc(x_113);
 lean_dec(x_75);
-x_113 = l_Lean_Meta_injectionCore___lambda__1___closed__8;
-x_114 = l_Lean_Meta_throwTacticEx___rarg(x_2, x_3, x_113, x_5, x_112);
+x_114 = l_Lean_Meta_injectionCore___lambda__1___closed__8;
+x_115 = l_Lean_Meta_throwTacticEx___rarg(x_2, x_3, x_114, x_5, x_113);
 lean_dec(x_5);
-return x_114;
+return x_115;
 }
 }
 else
 {
-uint8_t x_115; 
+uint8_t x_116; 
 lean_dec(x_54);
 lean_dec(x_50);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_115 = !lean_is_exclusive(x_75);
-if (x_115 == 0)
+x_116 = !lean_is_exclusive(x_75);
+if (x_116 == 0)
 {
 return x_75;
 }
 else
 {
-lean_object* x_116; lean_object* x_117; lean_object* x_118; 
-x_116 = lean_ctor_get(x_75, 0);
-x_117 = lean_ctor_get(x_75, 1);
+lean_object* x_117; lean_object* x_118; lean_object* x_119; 
+x_117 = lean_ctor_get(x_75, 0);
+x_118 = lean_ctor_get(x_75, 1);
+lean_inc(x_118);
 lean_inc(x_117);
-lean_inc(x_116);
 lean_dec(x_75);
-x_118 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_118, 0, x_116);
-lean_ctor_set(x_118, 1, x_117);
-return x_118;
+x_119 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_119, 0, x_117);
+lean_ctor_set(x_119, 1, x_118);
+return x_119;
 }
 }
 }
 else
 {
-uint8_t x_119; 
+uint8_t x_120; 
 lean_dec(x_54);
 lean_dec(x_50);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_119 = !lean_is_exclusive(x_72);
-if (x_119 == 0)
+x_120 = !lean_is_exclusive(x_72);
+if (x_120 == 0)
 {
 return x_72;
 }
 else
 {
-lean_object* x_120; lean_object* x_121; lean_object* x_122; 
-x_120 = lean_ctor_get(x_72, 0);
-x_121 = lean_ctor_get(x_72, 1);
+lean_object* x_121; lean_object* x_122; lean_object* x_123; 
+x_121 = lean_ctor_get(x_72, 0);
+x_122 = lean_ctor_get(x_72, 1);
+lean_inc(x_122);
 lean_inc(x_121);
-lean_inc(x_120);
 lean_dec(x_72);
-x_122 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_122, 0, x_120);
-lean_ctor_set(x_122, 1, x_121);
-return x_122;
+x_123 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_123, 0, x_121);
+lean_ctor_set(x_123, 1, x_122);
+return x_123;
 }
 }
 }
 }
 else
 {
-uint8_t x_123; 
+uint8_t x_124; 
 lean_dec(x_51);
 lean_dec(x_50);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_123 = !lean_is_exclusive(x_53);
-if (x_123 == 0)
+x_124 = !lean_is_exclusive(x_53);
+if (x_124 == 0)
 {
 return x_53;
 }
 else
 {
-lean_object* x_124; lean_object* x_125; lean_object* x_126; 
-x_124 = lean_ctor_get(x_53, 0);
-x_125 = lean_ctor_get(x_53, 1);
+lean_object* x_125; lean_object* x_126; lean_object* x_127; 
+x_125 = lean_ctor_get(x_53, 0);
+x_126 = lean_ctor_get(x_53, 1);
+lean_inc(x_126);
 lean_inc(x_125);
-lean_inc(x_124);
 lean_dec(x_53);
-x_126 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_126, 0, x_124);
-lean_ctor_set(x_126, 1, x_125);
-return x_126;
+x_127 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_127, 0, x_125);
+lean_ctor_set(x_127, 1, x_126);
+return x_127;
 }
 }
 }
@@ -815,141 +814,141 @@ return x_126;
 }
 else
 {
-uint8_t x_127; 
+uint8_t x_128; 
 lean_dec(x_33);
 lean_dec(x_30);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_127 = !lean_is_exclusive(x_35);
-if (x_127 == 0)
+x_128 = !lean_is_exclusive(x_35);
+if (x_128 == 0)
 {
 return x_35;
 }
 else
 {
-lean_object* x_128; lean_object* x_129; lean_object* x_130; 
-x_128 = lean_ctor_get(x_35, 0);
-x_129 = lean_ctor_get(x_35, 1);
+lean_object* x_129; lean_object* x_130; lean_object* x_131; 
+x_129 = lean_ctor_get(x_35, 0);
+x_130 = lean_ctor_get(x_35, 1);
+lean_inc(x_130);
 lean_inc(x_129);
-lean_inc(x_128);
 lean_dec(x_35);
-x_130 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_130, 0, x_128);
-lean_ctor_set(x_130, 1, x_129);
-return x_130;
+x_131 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_131, 0, x_129);
+lean_ctor_set(x_131, 1, x_130);
+return x_131;
 }
 }
 }
 else
 {
-uint8_t x_131; 
+uint8_t x_132; 
 lean_dec(x_30);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_131 = !lean_is_exclusive(x_32);
-if (x_131 == 0)
+x_132 = !lean_is_exclusive(x_32);
+if (x_132 == 0)
 {
 return x_32;
 }
 else
 {
-lean_object* x_132; lean_object* x_133; lean_object* x_134; 
-x_132 = lean_ctor_get(x_32, 0);
-x_133 = lean_ctor_get(x_32, 1);
+lean_object* x_133; lean_object* x_134; lean_object* x_135; 
+x_133 = lean_ctor_get(x_32, 0);
+x_134 = lean_ctor_get(x_32, 1);
+lean_inc(x_134);
 lean_inc(x_133);
-lean_inc(x_132);
 lean_dec(x_32);
-x_134 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_134, 0, x_132);
-lean_ctor_set(x_134, 1, x_133);
-return x_134;
+x_135 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_135, 0, x_133);
+lean_ctor_set(x_135, 1, x_134);
+return x_135;
 }
 }
 }
 else
 {
-uint8_t x_135; 
+uint8_t x_136; 
 lean_dec(x_28);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_135 = !lean_is_exclusive(x_29);
-if (x_135 == 0)
+x_136 = !lean_is_exclusive(x_29);
+if (x_136 == 0)
 {
 return x_29;
 }
 else
 {
-lean_object* x_136; lean_object* x_137; lean_object* x_138; 
-x_136 = lean_ctor_get(x_29, 0);
-x_137 = lean_ctor_get(x_29, 1);
+lean_object* x_137; lean_object* x_138; lean_object* x_139; 
+x_137 = lean_ctor_get(x_29, 0);
+x_138 = lean_ctor_get(x_29, 1);
+lean_inc(x_138);
 lean_inc(x_137);
-lean_inc(x_136);
 lean_dec(x_29);
-x_138 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_138, 0, x_136);
-lean_ctor_set(x_138, 1, x_137);
-return x_138;
+x_139 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_139, 0, x_137);
+lean_ctor_set(x_139, 1, x_138);
+return x_139;
 }
 }
 }
 }
 else
 {
-uint8_t x_139; 
+uint8_t x_140; 
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_139 = !lean_is_exclusive(x_11);
-if (x_139 == 0)
+x_140 = !lean_is_exclusive(x_11);
+if (x_140 == 0)
 {
 return x_11;
 }
 else
 {
-lean_object* x_140; lean_object* x_141; lean_object* x_142; 
-x_140 = lean_ctor_get(x_11, 0);
-x_141 = lean_ctor_get(x_11, 1);
+lean_object* x_141; lean_object* x_142; lean_object* x_143; 
+x_141 = lean_ctor_get(x_11, 0);
+x_142 = lean_ctor_get(x_11, 1);
+lean_inc(x_142);
 lean_inc(x_141);
-lean_inc(x_140);
 lean_dec(x_11);
-x_142 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_142, 0, x_140);
-lean_ctor_set(x_142, 1, x_141);
-return x_142;
+x_143 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_143, 0, x_141);
+lean_ctor_set(x_143, 1, x_142);
+return x_143;
 }
 }
 }
 else
 {
-uint8_t x_143; 
+uint8_t x_144; 
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_143 = !lean_is_exclusive(x_7);
-if (x_143 == 0)
+x_144 = !lean_is_exclusive(x_7);
+if (x_144 == 0)
 {
 return x_7;
 }
 else
 {
-lean_object* x_144; lean_object* x_145; lean_object* x_146; 
-x_144 = lean_ctor_get(x_7, 0);
-x_145 = lean_ctor_get(x_7, 1);
+lean_object* x_145; lean_object* x_146; lean_object* x_147; 
+x_145 = lean_ctor_get(x_7, 0);
+x_146 = lean_ctor_get(x_7, 1);
+lean_inc(x_146);
 lean_inc(x_145);
-lean_inc(x_144);
 lean_dec(x_7);
-x_146 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_146, 0, x_144);
-lean_ctor_set(x_146, 1, x_145);
-return x_146;
+x_147 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_147, 0, x_145);
+lean_ctor_set(x_147, 1, x_146);
+return x_147;
 }
 }
 }

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

@@ -246,6 +246,7 @@ lean_object* l_Lean_Parser_Term_letPatDecl;
 lean_object* l_Lean_Parser_Term_sortApp___closed__4;
 lean_object* l_Lean_Parser_Term_bnot___closed__2;
 lean_object* l_Lean_Parser_Term_typeAscription___elambda__1(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_band___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_and___closed__3;
@@ -378,6 +379,7 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__20;
 lean_object* l_Lean_Parser_Term_seqRight___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_match___elambda__1___closed__11;
+lean_object* l___regBuiltinParser_Lean_Parser_Term_let_x21(lean_object*);
 lean_object* l_Lean_Parser_Term_let___elambda__1___closed__7;
 lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1(lean_object*, lean_object*);
@@ -410,6 +412,7 @@ lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_let(lean_object*);
 lean_object* l_Lean_Parser_Term_doPat___closed__8;
 lean_object* l_Lean_Parser_Term_id___closed__4;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Term_show___closed__6;
 lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Term_listLit___closed__4;
@@ -454,6 +457,7 @@ lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__13;
 lean_object* l_Lean_Parser_Term_anonymousCtor___closed__9;
 lean_object* l_Lean_Parser_Term_sorry___closed__1;
 lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__3;
+lean_object* l_Lean_Parser_Term_let_x21___closed__6;
 lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_simpleBinder___closed__3;
 lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__3;
@@ -536,6 +540,7 @@ lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_equiv___closed__3;
 lean_object* l_Lean_Parser_Term_sorry___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__2;
+lean_object* l_Lean_Parser_Term_let_x21___closed__5;
 lean_object* l_Lean_Parser_Term_let___elambda__1___closed__5;
 lean_object* l_Lean_Parser_tacticParser(lean_object*);
 lean_object* l_Lean_Parser_Term_quotedName___elambda__1___closed__3;
@@ -632,6 +637,7 @@ lean_object* l_Lean_Parser_Term_uminus___closed__3;
 lean_object* l_Lean_Parser_Term_let___closed__1;
 lean_object* l_Lean_Parser_Term_namedHole___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_subtype___elambda__1___closed__4;
+lean_object* l_Lean_Parser_Term_let_x21___closed__3;
 lean_object* l_Lean_Parser_Term_typeAscription;
 lean_object* l_Lean_Parser_Term_sortApp;
 lean_object* l_Lean_Parser_Term_simpleBinder___closed__4;
@@ -1075,6 +1081,7 @@ lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___
 lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_char___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_explicitBinder___closed__1;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_dollarProj___closed__1;
 lean_object* l_Lean_Parser_Term_do;
 lean_object* l_Lean_Parser_Term_seqRight___closed__3;
@@ -1083,6 +1090,7 @@ lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_nonEmptySeq___elambd
 lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_bnot(lean_object*);
 lean_object* l_Lean_Parser_Term_binderTactic___closed__1;
+lean_object* l_Lean_Parser_Term_let_x21;
 lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_bnot___elambda__1___closed__2;
@@ -1105,6 +1113,7 @@ lean_object* l_Lean_Parser_Term_explicitUniv___closed__4;
 lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__12(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_append___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_proj___closed__2;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__5;
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_fun___closed__4;
 lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__3;
@@ -1391,6 +1400,7 @@ lean_object* l_Lean_Parser_Term_simpleBinder;
 lean_object* l_Lean_Parser_Term_bor___elambda__1___closed__3;
 lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_div___elambda__1___closed__3;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Term_doExpr___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_let___closed__5;
 lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__8;
@@ -1493,6 +1503,7 @@ lean_object* l_Lean_Parser_Term_hole___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__2;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_mapConst(lean_object*);
 lean_object* l_Lean_Parser_Term_inaccessible___closed__5;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_typeAscription___closed__4;
 lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_binderType___closed__2;
@@ -1632,6 +1643,7 @@ lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_if___closed__6;
 lean_object* l_Lean_Parser_Term_letIdDecl___closed__2;
 lean_object* l_Lean_Parser_Term_char;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_structInstField___closed__5;
 lean_object* l_Lean_Parser_Term_matchAlts___closed__2;
 lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__6;
@@ -1795,6 +1807,7 @@ lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Parser_Term_funBinder___closed__2;
 lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__9;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_explicit;
 lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__7;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_arrow(lean_object*);
@@ -1852,6 +1865,7 @@ lean_object* l_Lean_Parser_Term_ne___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_paren___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_explicitUniv___closed__11;
 lean_object* l_Lean_Parser_Term_arrayLit___closed__1;
+lean_object* l_Lean_Parser_Term_let_x21___closed__1;
 lean_object* l_Lean_Parser_Term_nomatch___closed__5;
 lean_object* l_Lean_Parser_Term_beq___closed__1;
 lean_object* l_Lean_Parser_Term_fun___closed__2;
@@ -1916,6 +1930,7 @@ lean_object* l_Lean_Parser_Term_nomatch___closed__3;
 lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_add___closed__3;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Term_structInst;
 lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Tactic_nonEmptySeq___closed__1;
@@ -1927,6 +1942,7 @@ lean_object* l_Lean_Parser_Term_char___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__6;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_borrowed(lean_object*);
 lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__1;
@@ -2031,6 +2047,7 @@ lean_object* l_Lean_Parser_Term_namedHole___closed__1;
 lean_object* l_Lean_Parser_Term_map;
 lean_object* l_Lean_Parser_Term_unicodeInfixR(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9;
+lean_object* l_Lean_Parser_Term_let_x21___closed__2;
 lean_object* l_Lean_Parser_Term_forall___closed__6;
 lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_modN___closed__1;
@@ -2065,6 +2082,7 @@ extern lean_object* l_Lean_Parser_Level_max___closed__2;
 lean_object* l_Lean_Parser_Term_binderTactic___closed__5;
 lean_object* l_Lean_Parser_Term_doId___elambda__1___closed__3;
 lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__7(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_let_x21___closed__4;
 lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_letIdDecl___closed__6;
 lean_object* l_Lean_Parser_Term_app___closed__4;
@@ -34868,6 +34886,578 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
 return x_6;
 }
 }
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("let!");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_mkAppStx___closed__6;
+x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_2 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__1;
+x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__3;
+x_3 = 1;
+x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__5() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("let! ");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__5;
+x_2 = l_String_trim(x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__7() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Char_HasRepr___closed__1;
+x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6;
+x_3 = lean_string_append(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__8() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__7;
+x_2 = l_Char_HasRepr___closed__1;
+x_3 = lean_string_append(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__9() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__8;
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
+return x_3;
+}
+}
+lean_object* l_Lean_Parser_Term_let_x21___elambda__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_3 = l_Lean_Parser_Term_let_x21___elambda__1___closed__4;
+x_4 = lean_ctor_get(x_3, 1);
+lean_inc(x_4);
+lean_inc(x_2);
+lean_inc(x_1);
+x_5 = l_Lean_Parser_tryAnti(x_1, x_2);
+if (x_5 == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_42; lean_object* x_43; lean_object* x_44; 
+lean_dec(x_4);
+x_6 = lean_ctor_get(x_2, 0);
+lean_inc(x_6);
+x_7 = lean_array_get_size(x_6);
+lean_dec(x_6);
+x_42 = lean_ctor_get(x_2, 1);
+lean_inc(x_42);
+lean_inc(x_1);
+x_43 = l_Lean_Parser_tokenFn(x_1, x_2);
+x_44 = lean_ctor_get(x_43, 3);
+lean_inc(x_44);
+if (lean_obj_tag(x_44) == 0)
+{
+lean_object* x_45; lean_object* x_46; 
+x_45 = lean_ctor_get(x_43, 0);
+lean_inc(x_45);
+x_46 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_45);
+lean_dec(x_45);
+if (lean_obj_tag(x_46) == 2)
+{
+lean_object* x_47; lean_object* x_48; uint8_t x_49; 
+x_47 = lean_ctor_get(x_46, 1);
+lean_inc(x_47);
+lean_dec(x_46);
+x_48 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6;
+x_49 = lean_string_dec_eq(x_47, x_48);
+lean_dec(x_47);
+if (x_49 == 0)
+{
+lean_object* x_50; lean_object* x_51; 
+x_50 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9;
+x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_50, x_42);
+x_8 = x_51;
+goto block_41;
+}
+else
+{
+lean_dec(x_42);
+x_8 = x_43;
+goto block_41;
+}
+}
+else
+{
+lean_object* x_52; lean_object* x_53; 
+lean_dec(x_46);
+x_52 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9;
+x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_52, x_42);
+x_8 = x_53;
+goto block_41;
+}
+}
+else
+{
+lean_object* x_54; lean_object* x_55; 
+lean_dec(x_44);
+x_54 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9;
+x_55 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_54, x_42);
+x_8 = x_55;
+goto block_41;
+}
+block_41:
+{
+lean_object* x_9; 
+x_9 = lean_ctor_get(x_8, 3);
+lean_inc(x_9);
+if (lean_obj_tag(x_9) == 0)
+{
+lean_object* x_10; lean_object* x_11; 
+lean_inc(x_1);
+x_10 = l_Lean_Parser_Term_letDecl___elambda__1(x_1, x_8);
+x_11 = lean_ctor_get(x_10, 3);
+lean_inc(x_11);
+if (lean_obj_tag(x_11) == 0)
+{
+lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_12 = lean_ctor_get(x_10, 1);
+lean_inc(x_12);
+lean_inc(x_1);
+x_13 = l_Lean_Parser_tokenFn(x_1, x_10);
+x_14 = lean_ctor_get(x_13, 3);
+lean_inc(x_14);
+if (lean_obj_tag(x_14) == 0)
+{
+lean_object* x_15; lean_object* x_16; 
+x_15 = lean_ctor_get(x_13, 0);
+lean_inc(x_15);
+x_16 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_15);
+lean_dec(x_15);
+if (lean_obj_tag(x_16) == 2)
+{
+lean_object* x_17; lean_object* x_18; uint8_t x_19; 
+x_17 = lean_ctor_get(x_16, 1);
+lean_inc(x_17);
+lean_dec(x_16);
+x_18 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1;
+x_19 = lean_string_dec_eq(x_17, x_18);
+lean_dec(x_17);
+if (x_19 == 0)
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+lean_dec(x_1);
+x_20 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4;
+x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_20, x_12);
+x_22 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_7);
+return x_23;
+}
+else
+{
+lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+lean_dec(x_12);
+x_24 = l_Lean_Parser_termParser___closed__2;
+x_25 = lean_unsigned_to_nat(0u);
+x_26 = l_Lean_Parser_categoryParser___elambda__1(x_24, x_25, x_1, x_13);
+x_27 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_7);
+return x_28;
+}
+}
+else
+{
+lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+lean_dec(x_16);
+lean_dec(x_1);
+x_29 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4;
+x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_29, x_12);
+x_31 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_7);
+return x_32;
+}
+}
+else
+{
+lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+lean_dec(x_14);
+lean_dec(x_1);
+x_33 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4;
+x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_33, x_12);
+x_35 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_36 = l_Lean_Parser_ParserState_mkNode(x_34, x_35, x_7);
+return x_36;
+}
+}
+else
+{
+lean_object* x_37; lean_object* x_38; 
+lean_dec(x_11);
+lean_dec(x_1);
+x_37 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_38 = l_Lean_Parser_ParserState_mkNode(x_10, x_37, x_7);
+return x_38;
+}
+}
+else
+{
+lean_object* x_39; lean_object* x_40; 
+lean_dec(x_9);
+lean_dec(x_1);
+x_39 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_40 = l_Lean_Parser_ParserState_mkNode(x_8, x_39, x_7);
+return x_40;
+}
+}
+}
+else
+{
+lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; 
+x_56 = lean_ctor_get(x_2, 0);
+lean_inc(x_56);
+x_57 = lean_array_get_size(x_56);
+lean_dec(x_56);
+x_58 = lean_ctor_get(x_2, 1);
+lean_inc(x_58);
+lean_inc(x_1);
+x_59 = lean_apply_2(x_4, x_1, x_2);
+x_60 = lean_ctor_get(x_59, 3);
+lean_inc(x_60);
+if (lean_obj_tag(x_60) == 0)
+{
+lean_dec(x_58);
+lean_dec(x_57);
+lean_dec(x_1);
+return x_59;
+}
+else
+{
+lean_object* x_61; lean_object* x_62; uint8_t x_63; 
+x_61 = lean_ctor_get(x_60, 0);
+lean_inc(x_61);
+lean_dec(x_60);
+x_62 = lean_ctor_get(x_59, 1);
+lean_inc(x_62);
+x_63 = lean_nat_dec_eq(x_62, x_58);
+lean_dec(x_62);
+if (x_63 == 0)
+{
+lean_dec(x_61);
+lean_dec(x_58);
+lean_dec(x_57);
+lean_dec(x_1);
+return x_59;
+}
+else
+{
+lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_107; lean_object* x_108; 
+lean_inc(x_58);
+x_64 = l_Lean_Parser_ParserState_restore(x_59, x_57, x_58);
+lean_dec(x_57);
+x_65 = lean_ctor_get(x_64, 0);
+lean_inc(x_65);
+x_66 = lean_array_get_size(x_65);
+lean_dec(x_65);
+lean_inc(x_1);
+x_107 = l_Lean_Parser_tokenFn(x_1, x_64);
+x_108 = lean_ctor_get(x_107, 3);
+lean_inc(x_108);
+if (lean_obj_tag(x_108) == 0)
+{
+lean_object* x_109; lean_object* x_110; 
+x_109 = lean_ctor_get(x_107, 0);
+lean_inc(x_109);
+x_110 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_109);
+lean_dec(x_109);
+if (lean_obj_tag(x_110) == 2)
+{
+lean_object* x_111; lean_object* x_112; uint8_t x_113; 
+x_111 = lean_ctor_get(x_110, 1);
+lean_inc(x_111);
+lean_dec(x_110);
+x_112 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6;
+x_113 = lean_string_dec_eq(x_111, x_112);
+lean_dec(x_111);
+if (x_113 == 0)
+{
+lean_object* x_114; lean_object* x_115; 
+x_114 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9;
+lean_inc(x_58);
+x_115 = l_Lean_Parser_ParserState_mkErrorsAt(x_107, x_114, x_58);
+x_67 = x_115;
+goto block_106;
+}
+else
+{
+x_67 = x_107;
+goto block_106;
+}
+}
+else
+{
+lean_object* x_116; lean_object* x_117; 
+lean_dec(x_110);
+x_116 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9;
+lean_inc(x_58);
+x_117 = l_Lean_Parser_ParserState_mkErrorsAt(x_107, x_116, x_58);
+x_67 = x_117;
+goto block_106;
+}
+}
+else
+{
+lean_object* x_118; lean_object* x_119; 
+lean_dec(x_108);
+x_118 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9;
+lean_inc(x_58);
+x_119 = l_Lean_Parser_ParserState_mkErrorsAt(x_107, x_118, x_58);
+x_67 = x_119;
+goto block_106;
+}
+block_106:
+{
+lean_object* x_68; 
+x_68 = lean_ctor_get(x_67, 3);
+lean_inc(x_68);
+if (lean_obj_tag(x_68) == 0)
+{
+lean_object* x_69; lean_object* x_70; 
+lean_inc(x_1);
+x_69 = l_Lean_Parser_Term_letDecl___elambda__1(x_1, x_67);
+x_70 = lean_ctor_get(x_69, 3);
+lean_inc(x_70);
+if (lean_obj_tag(x_70) == 0)
+{
+lean_object* x_71; lean_object* x_72; lean_object* x_73; 
+x_71 = lean_ctor_get(x_69, 1);
+lean_inc(x_71);
+lean_inc(x_1);
+x_72 = l_Lean_Parser_tokenFn(x_1, x_69);
+x_73 = lean_ctor_get(x_72, 3);
+lean_inc(x_73);
+if (lean_obj_tag(x_73) == 0)
+{
+lean_object* x_74; lean_object* x_75; 
+x_74 = lean_ctor_get(x_72, 0);
+lean_inc(x_74);
+x_75 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_74);
+lean_dec(x_74);
+if (lean_obj_tag(x_75) == 2)
+{
+lean_object* x_76; lean_object* x_77; uint8_t x_78; 
+x_76 = lean_ctor_get(x_75, 1);
+lean_inc(x_76);
+lean_dec(x_75);
+x_77 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1;
+x_78 = lean_string_dec_eq(x_76, x_77);
+lean_dec(x_76);
+if (x_78 == 0)
+{
+lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; 
+lean_dec(x_1);
+x_79 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4;
+x_80 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_79, x_71);
+x_81 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_82 = l_Lean_Parser_ParserState_mkNode(x_80, x_81, x_66);
+x_83 = l_Lean_Parser_mergeOrElseErrors(x_82, x_61, x_58);
+lean_dec(x_58);
+return x_83;
+}
+else
+{
+lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; 
+lean_dec(x_71);
+x_84 = l_Lean_Parser_termParser___closed__2;
+x_85 = lean_unsigned_to_nat(0u);
+x_86 = l_Lean_Parser_categoryParser___elambda__1(x_84, x_85, x_1, x_72);
+x_87 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_88 = l_Lean_Parser_ParserState_mkNode(x_86, x_87, x_66);
+x_89 = l_Lean_Parser_mergeOrElseErrors(x_88, x_61, x_58);
+lean_dec(x_58);
+return x_89;
+}
+}
+else
+{
+lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; 
+lean_dec(x_75);
+lean_dec(x_1);
+x_90 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4;
+x_91 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_90, x_71);
+x_92 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_93 = l_Lean_Parser_ParserState_mkNode(x_91, x_92, x_66);
+x_94 = l_Lean_Parser_mergeOrElseErrors(x_93, x_61, x_58);
+lean_dec(x_58);
+return x_94;
+}
+}
+else
+{
+lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; 
+lean_dec(x_73);
+lean_dec(x_1);
+x_95 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4;
+x_96 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_95, x_71);
+x_97 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_98 = l_Lean_Parser_ParserState_mkNode(x_96, x_97, x_66);
+x_99 = l_Lean_Parser_mergeOrElseErrors(x_98, x_61, x_58);
+lean_dec(x_58);
+return x_99;
+}
+}
+else
+{
+lean_object* x_100; lean_object* x_101; lean_object* x_102; 
+lean_dec(x_70);
+lean_dec(x_1);
+x_100 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_101 = l_Lean_Parser_ParserState_mkNode(x_69, x_100, x_66);
+x_102 = l_Lean_Parser_mergeOrElseErrors(x_101, x_61, x_58);
+lean_dec(x_58);
+return x_102;
+}
+}
+else
+{
+lean_object* x_103; lean_object* x_104; lean_object* x_105; 
+lean_dec(x_68);
+lean_dec(x_1);
+x_103 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_104 = l_Lean_Parser_ParserState_mkNode(x_67, x_103, x_66);
+x_105 = l_Lean_Parser_mergeOrElseErrors(x_104, x_61, x_58);
+lean_dec(x_58);
+return x_105;
+}
+}
+}
+}
+}
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6;
+x_2 = l_Lean_Parser_Term_if___closed__1;
+x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Term_let_x21___closed__1;
+x_2 = l_Lean_Parser_Term_let___closed__3;
+x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Term_let_x21___closed__2;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__4;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Term_let_x21___closed__3;
+x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___closed__5() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_let_x21___elambda__1), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Term_let_x21___closed__4;
+x_2 = l_Lean_Parser_Term_let_x21___closed__5;
+x_3 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Term_let_x21() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_Parser_Term_let_x21___closed__6;
+return x_1;
+}
+}
+lean_object* l___regBuiltinParser_Lean_Parser_Term_let_x21(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+x_2 = l_Lean_Parser_termParser___closed__2;
+x_3 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
+x_4 = 1;
+x_5 = l_Lean_Parser_Term_let_x21;
+x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
+return x_6;
+}
+}
 lean_object* _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__1() {
 _start:
 {
@@ -51088,6 +51678,41 @@ lean_mark_persistent(l_Lean_Parser_Term_let);
 res = l___regBuiltinParser_Lean_Parser_Term_let(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__1 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__1();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__1);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__2 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__2();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__2);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__3 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__3();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__3);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__4 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__4();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__4);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__5 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__5();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__5);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__6 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__6();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__6);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__7 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__7();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__7);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__8 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__8();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__8);
+l_Lean_Parser_Term_let_x21___elambda__1___closed__9 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__9();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__9);
+l_Lean_Parser_Term_let_x21___closed__1 = _init_l_Lean_Parser_Term_let_x21___closed__1();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__1);
+l_Lean_Parser_Term_let_x21___closed__2 = _init_l_Lean_Parser_Term_let_x21___closed__2();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__2);
+l_Lean_Parser_Term_let_x21___closed__3 = _init_l_Lean_Parser_Term_let_x21___closed__3();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__3);
+l_Lean_Parser_Term_let_x21___closed__4 = _init_l_Lean_Parser_Term_let_x21___closed__4();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__4);
+l_Lean_Parser_Term_let_x21___closed__5 = _init_l_Lean_Parser_Term_let_x21___closed__5();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__5);
+l_Lean_Parser_Term_let_x21___closed__6 = _init_l_Lean_Parser_Term_let_x21___closed__6();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__6);
+l_Lean_Parser_Term_let_x21 = _init_l_Lean_Parser_Term_let_x21();
+lean_mark_persistent(l_Lean_Parser_Term_let_x21);
+res = l___regBuiltinParser_Lean_Parser_Term_let_x21(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Lean_Parser_Term_leftArrow___elambda__1___closed__1 = _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__1();
 lean_mark_persistent(l_Lean_Parser_Term_leftArrow___elambda__1___closed__1);
 l_Lean_Parser_Term_leftArrow___elambda__1___closed__2 = _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__2();