chore: update stage0

stage0/src/Init/Classical.lean

@@ -26,36 +26,36 @@ theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose
 
 /- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
 theorem em (p : Prop) : p ∨ ¬p :=
-  let U (x : Prop) : Prop := x = True ∨ p;
-  let V (x : Prop) : Prop := x = False ∨ p;
-  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩;
-  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩;
-  let u : Prop := choose exU;
-  let v : Prop := choose exV;
-  have uDef : U u := choose_spec exU;
-  have vDef : V v := choose_spec exV;
-  have notUvOrP : u ≠ v ∨ p :=
-    match uDef, vDef with
+  let U (x : Prop) : Prop := x = True ∨ p
+  let V (x : Prop) : Prop := x = False ∨ p
+  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
+  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
+  let u : Prop := choose exU
+  let v : Prop := choose exV
+  have u_def : U u := choose_spec exU
+  have v_def : V v := choose_spec exV
+  have not_uv_or_p : u ≠ v ∨ p :=
+    match u_def, v_def with
     | Or.inr h, _ => Or.inr h
     | _, Or.inr h => Or.inr h
     | Or.inl hut, Or.inl hvf =>
-      have hne : u ≠ v := hvf.symm ▸ hut.symm ▸ true_ne_false
+      have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
       Or.inl hne
-  have pImpliesUv : p → u = v :=
+  have p_implies_uv : p → u = v :=
     fun hp =>
     have hpred : U = V :=
       funext fun x =>
         have hl : (x = True ∨ p) → (x = False ∨ p) :=
-          fun a => Or.inr hp;
+          fun _ => Or.inr hp
         have hr : (x = False ∨ p) → (x = True ∨ p) :=
-          fun a => Or.inr hp;
+          fun _ => Or.inr hp
         show (x = True ∨ p) = (x = False ∨ p) from
-          propext (Iff.intro hl hr);
-    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV :=
-      hpred ▸ fun exU exV => rfl;
-    show u = v from h₀ ..;
-  match notUvOrP with
-  | Or.inl hne => Or.inr (mt pImpliesUv hne)
+          propext (Iff.intro hl hr)
+    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
+      rw [hpred]; intros; rfl
+    show u = v from h₀ _ _
+  match not_uv_or_p with
+  | Or.inl hne => Or.inr (mt p_implies_uv hne)
   | Or.inr h   => Or.inl h
 
 theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ x : α, True
@@ -114,10 +114,10 @@ theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Pr
 theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, ∃ y, p x y) ↔ ∃ (f : ∀ x, b x), ∀ x, p x (f x) :=
   ⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩
 
-theorem propComplete (a : Prop) : a = True ∨ a = False := by
-  cases em a with
-  | inl _  => apply Or.inl; apply propext; apply Iff.intro; { intros; apply True.intro }; { intro; assumption }
-  | inr hn => apply Or.inr; apply propext; apply Iff.intro; { intro h; exact hn h }; { intro h; apply False.elim h }
+theorem propComplete (a : Prop) : a = True ∨ a = False :=
+  match em a with
+  | Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha)))
+  | Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
 
 -- this supercedes byCases in Decidable
 theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=

stage0/src/Init/Notation.lean

@@ -353,6 +353,8 @@ def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Sy
 
 syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
 
+syntax (name := injections) "injections" : tactic
+
 syntax simpPre   := "↓"
 syntax simpPost  := "↑"
 syntax simpLemma := (simpPre <|> simpPost)? ("←" <|> "<-")? term

stage0/src/Lean/Elab/Syntax.lean

@@ -231,9 +231,16 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
 
 @[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do
   let catName  := stx[1].getId
+  let catBehavior :=
+    if stx[2].isNone then
+      Parser.LeadingIdentBehavior.default
+    else if stx[2][3].getKind == ``Parser.Command.catBehaviorBoth then
+      Parser.LeadingIdentBehavior.both
+    else
+      Parser.LeadingIdentBehavior.symbol
   let attrName := catName.appendAfter "Parser"
   let env ← getEnv
-  let env ← liftIO $ Parser.registerParserCategory env attrName catName
+  let env ← Parser.registerParserCategory env attrName catName catBehavior
   setEnv env
   declareSyntaxCatQuotParser catName
 

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

@@ -23,8 +23,14 @@ private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Uni
   let fvarId ← elabAsFVar stx[1]
   let ids := getInjectionNewIds stx[2]
   liftMetaTactic fun mvarId => do
-    match (← Meta.injection mvarId fvarId ids (!ids.isEmpty)) with
-    | Meta.InjectionResult.solved                      => checkUnusedIds mvarId ids; pure []
-    | Meta.InjectionResult.subgoal mvarId' _ unusedIds => checkUnusedIds mvarId unusedIds; pure [mvarId']
+    match (← Meta.injection mvarId fvarId ids) with
+    | Meta.InjectionResult.solved                      => checkUnusedIds mvarId ids; return []
+    | Meta.InjectionResult.subgoal mvarId' _ unusedIds => checkUnusedIds mvarId unusedIds; return [mvarId']
+
+@[builtinTactic «injections»] def evalInjections : Tactic := fun stx => do
+  liftMetaTactic fun mvarId => do
+    match (← Meta.injections mvarId) with
+    | none => return []
+    | some mvarId => return [mvarId]
 
 end Lean.Elab.Tactic

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

@@ -5,16 +5,33 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Split
 import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Location
 
 namespace Lean.Elab.Tactic
 open Meta
 
-@[builtinTactic Lean.Parser.Tactic.split] def evalSplit : Tactic := fun stx =>
-  -- TODO: process arguments
+@[builtinTactic Lean.Parser.Tactic.split] def evalSplit : Tactic := fun stx => do
+  unless stx[1].isNone do
+    throwError "'split' tatic, term to split is not supported yet"
   liftMetaTactic fun mvarId => do
-    if let some mvarIds ← splitTarget? mvarId then
+    let loc := expandOptLocation stx[2]
+    match loc with
+    | Location.targets hUserNames simplifyTarget =>
+      if (hUserNames.size > 0 && simplifyTarget) || hUserNames.size > 1 then
+        throwErrorAt stx[2] "'split' tactic failed, select a single target to split"
+      if simplifyTarget then
+        let some mvarIds ← splitTarget? mvarId | throwError "'split' tactic failed"
+        return mvarIds
+      else
+        let fvarId := (← getLocalDeclFromUserName hUserNames[0]).fvarId
+        let some mvarIds ← splitLocalDecl? mvarId fvarId | throwError "'split' tactic failed"
+        return mvarIds
+    | Location.wildcard =>
+      let fvarIds ← getNondepPropHyps mvarId
+      for fvarId in fvarIds do
+        if let some mvarIds ← splitLocalDecl? mvarId fvarId then
+          return mvarIds
+      let some mvarIds ← splitTarget? mvarId | throwError "'split' tactic failed"
       return mvarIds
-    else
-      throwError "'split' tactic failed"
 
 end Lean.Elab.Tactic

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

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.AppBuilder
+import Lean.Meta.MatchUtil
 import Lean.Meta.Tactic.Clear
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Intro
@@ -50,7 +51,8 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
             let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
             assignExprMVar mvarId (mkApp val newMVar)
             let mvarId ← tryClear newMVar.mvarId! fvarId
-            /- Recall that `noConfusion` does not include equalities for propositions since they are trivial due to proof irrelevance. -/
+            /- Recall that `noConfusion` does not include equalities for
+               propositions since they are trivial due to proof irrelevance. -/
             let numPropFields ← getCtorNumPropFields aCtor
             return InjectionResultCore.subgoal mvarId (aCtor.numFields - numPropFields)
           | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
@@ -60,7 +62,7 @@ inductive InjectionResult where
   | solved
   | subgoal (mvarId : MVarId) (newEqs : Array FVarId) (remainingNames : List Name)
 
-private def heqToEq (mvarId : MVarId) (fvarId : FVarId) : MetaM (FVarId × MVarId) :=
+private def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool) : MetaM (FVarId × MVarId) :=
   withMVarContext mvarId do
    let decl ← getLocalDecl fvarId
    let type ← whnf decl.type
@@ -70,29 +72,55 @@ private def heqToEq (mvarId : MVarId) (fvarId : FVarId) : MetaM (FVarId × MVarI
      if (← isDefEq α β) then
        let pr ← mkEqOfHEq (mkFVar fvarId)
        let eq ← mkEq a b
-       let mvarId ← assert mvarId decl.userName eq pr
-       let mvarId ← clear mvarId fvarId
-       let (fvarId, mvarId) ← intro1P mvarId
-       pure (fvarId, mvarId)
+       let mut mvarId ← assert mvarId decl.userName eq pr
+       if tryToClear then
+         mvarId ← tryClear mvarId fvarId
+       let (fvarId, mvarId') ← intro1P mvarId
+       return (fvarId, mvarId')
      else
-       pure (fvarId, mvarId)
+       return (fvarId, mvarId)
 
-def injectionIntro : Nat → MVarId → Array FVarId → List Name → MetaM InjectionResult
-  | 0, mvarId, fvarIds, remainingNames =>
-    pure $ InjectionResult.subgoal mvarId fvarIds remainingNames
-  | n+1, mvarId, fvarIds, name::remainingNames => do
-    let (fvarId, mvarId) ← intro mvarId name
-    let (fvarId, mvarId) ← heqToEq mvarId fvarId
-    injectionIntro n mvarId (fvarIds.push fvarId) remainingNames
-  | n+1, mvarId, fvarIds, [] => do
-    let (fvarId, mvarId) ← intro1 mvarId
-    let (fvarId, mvarId) ← heqToEq mvarId fvarId
-    injectionIntro n mvarId (fvarIds.push fvarId) []
+def injectionIntro (mvarId : MVarId) (numEqs : Nat) (newNames : List Name) (tryToClear := true) : MetaM InjectionResult :=
+  let rec go : Nat → MVarId → Array FVarId → List Name → MetaM InjectionResult
+    | 0, mvarId, fvarIds, remainingNames =>
+      return InjectionResult.subgoal mvarId fvarIds remainingNames
+    | n+1, mvarId, fvarIds, name::remainingNames => do
+      let (fvarId, mvarId) ← intro mvarId name
+      let (fvarId, mvarId) ← heqToEq mvarId fvarId tryToClear
+      go n mvarId (fvarIds.push fvarId) remainingNames
+    | n+1, mvarId, fvarIds, [] => do
+      let (fvarId, mvarId) ← intro1 mvarId
+      let (fvarId, mvarId) ← heqToEq mvarId fvarId tryToClear
+      go n mvarId (fvarIds.push fvarId) []
+  go numEqs mvarId #[] newNames
 
-def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) (useUnusedNames : Bool := true) : MetaM InjectionResult := do
+def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) : MetaM InjectionResult := do
   match (← injectionCore mvarId fvarId) with
   | InjectionResultCore.solved                => pure InjectionResult.solved
-  | InjectionResultCore.subgoal mvarId numEqs =>
-    injectionIntro numEqs mvarId #[] newNames
+  | InjectionResultCore.subgoal mvarId numEqs => injectionIntro mvarId numEqs newNames
+
+partial def injections (mvarId : MVarId) (maxDepth : Nat := 5) : MetaM (Option MVarId) :=
+  withMVarContext mvarId do
+    let fvarIds := (← getLCtx).getFVarIds
+    go maxDepth fvarIds.toList mvarId
+where
+  go : Nat → List FVarId → MVarId → MetaM (Option MVarId)
+    | 0,   _,  _      => throwTacticEx `injections mvarId "recursion depth exceeded"
+    | _,   [], mvarId => return mvarId
+    | d+1, fvarId :: fvarIds, mvarId => do
+      let cont := do
+        go (d+1) fvarIds mvarId
+      if let some (_, lhs, rhs) ← matchEq? (← getLocalDecl fvarId).type then
+        let lhs ← whnf lhs
+        let rhs ← whnf rhs
+        if lhs.isNatLit && rhs.isNatLit then cont
+        else
+          try
+            match (← injection mvarId fvarId) with
+            | InjectionResult.solved  => return none
+            | InjectionResult.subgoal mvarId newEqs _ =>
+              withMVarContext mvarId <| go d (newEqs.toList ++ fvarIds) mvarId
+          catch _ => cont
+      else cont
 
 end Lean.Meta

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

@@ -425,6 +425,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (disc
       if type != type' then
         let mvarId ← assert mvarId localDecl.userName type' value
         let mvarId ← tryClear mvarId localDecl.fvarId
+        let (fvarId, mvarId) ← intro1P mvarId
         return some (fvarId, mvarId)
       else
         return some (fvarId, mvarId)

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

@@ -57,7 +57,7 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
   let some app ← matchMatcherApp? e | throwError "match application expected"
   let (discrFVarIds, mvarId) ← generalizeMatchDiscrs mvarId app.discrs
   trace[Meta.debug] "split [1]:\n{MessageData.ofGoal mvarId}"
-  let (reverted, mvarId) ← revert mvarId discrFVarIds
+  let (reverted, mvarId) ← revert mvarId discrFVarIds (preserveOrder := true)
   let (discrFVarIds, mvarId) ← introNP mvarId discrFVarIds.size
   let numExtra := reverted.size - discrFVarIds.size
   let discrs := discrFVarIds.map mkFVar
@@ -107,4 +107,18 @@ def splitTarget? (mvarId : MVarId) : MetaM (Option (List MVarId)) := commitWhenS
   else
     return none
 
+def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId)) := commitWhenSome? do
+  withMVarContext mvarId do
+    if let some e := findSplit? (← getEnv) (← inferType (mkFVar fvarId)) then
+      if e.isIte || e.isDIte then
+        return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂]
+      else
+        let (fvarIds, mvarId) ← revert mvarId #[fvarId]
+        let num := fvarIds.size
+        let mvarIds ← splitMatch mvarId e
+        let mvarIds ← mvarIds.mapM fun mvarId => return (← introNP mvarId num).2
+        return some mvarIds
+    else
+      return none
+
 end Lean.Meta

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

@@ -91,6 +91,13 @@ def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
   else
     unreachable!
 
+def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
+  let mut ctx ← getSimpContext
+  if let some (_, mvarId') ← simpLocalDecl mvarId fvarId ctx discharge? then
+    return mvarId'
+  else
+    unreachable!
+
 def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := commitWhenSome? do
   if let some (s₁, s₂) ← splitIfAt? mvarId (← getMVarType mvarId) hName? then
     let mvarId₁ ← simpIfTarget s₁.mvarId
@@ -102,6 +109,18 @@ def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Opt
   else
     return none
 
+def splitIfLocalDecl? (mvarId : MVarId) (fvarId : FVarId) (hName? : Option Name := none) : MetaM (Option (MVarId × MVarId)) := commitWhenSome? do
+  withMVarContext mvarId do
+    if let some (s₁, s₂) ← splitIfAt? mvarId (← inferType (mkFVar fvarId)) hName? then
+      let mvarId₁ ← simpIfLocalDecl s₁.mvarId fvarId
+      let mvarId₂ ← simpIfLocalDecl s₂.mvarId fvarId
+      if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then
+        return none
+      else
+        return some (mvarId₁, mvarId₂)
+    else
+      return none
+
 builtin_initialize registerTraceClass `Meta.Tactic.splitIf
 
 end Lean.Meta

stage0/src/Lean/Parser/Basic.lean

@@ -1593,8 +1593,7 @@ inductive LeadingIdentBehavior where
   | default
   | symbol
   | both
-  deriving Inhabited, BEq
-
+  deriving Inhabited, BEq, Repr
 
 /--
   Each parser category is implemented using a Pratt's parser.

stage0/src/Lean/Parser/Syntax.lean

@@ -71,7 +71,10 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Par
 @[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser optional docComment >> Term.attrKind >> "macro_rules" >>  optKind >> Term.matchAlts)
 @[builtinCommandParser] def «syntax»      := leading_parser optional docComment >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident
 @[builtinCommandParser] def syntaxAbbrev  := leading_parser "syntax " >> ident >> " := " >> many1 syntaxParser
-@[builtinCommandParser] def syntaxCat     := leading_parser "declare_syntax_cat " >> ident
+def catBehaviorBoth   := leading_parser nonReservedSymbol "both"
+def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"
+def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")
+@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident >> catBehavior
 def macroArg  := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec
 def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> termParser
 def macroTailTactic   : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1

stage0/stdlib/Lean/Elab/Syntax.c

@@ -170,6 +170,7 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabSynta
 lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_toParserDescr_resolveParserName___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Term_toParserDescr_resolveParserName___spec__11(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Term_withNotFirst(lean_object*);
+static lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1;
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandNoKindMacroRulesAux___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___spec__1___closed__5;
 lean_object* l_String_mapAux___at_Lean_Elab_Command_mkNameFromParserSyntax_visit___spec__2(lean_object*, lean_object*);
@@ -300,7 +301,7 @@ lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__2;
 lean_object* l_String_capitalize(lean_object*);
-lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550_(lean_object*);
+lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567_(lean_object*);
 lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Term_toParserDescr_resolveParserName___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_elabSyntaxAbbrev___closed__16;
 lean_object* l_Lean_Elab_Command_elabSyntax_match__2___rarg(lean_object*, lean_object*);
@@ -445,6 +446,7 @@ lean_object* l_Lean_Elab_Command_inferMacroRulesAltKind(lean_object*, lean_objec
 static lean_object* l_Lean_Elab_Command_elabSyntax___lambda__10___closed__1;
 static lean_object* l_Lean_Elab_Term_toParserDescr_processParserCategory___lambda__1___closed__8;
 lean_object* l_Lean_Parser_registerParserCategory(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
+static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567____closed__1;
 lean_object* l_Lean_Elab_Term_resetMessageLog(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_filterAux___at_Lean_resolveGlobalConstCore___spec__1(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__61;
@@ -632,7 +634,6 @@ uint8_t l_List_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_mkConstWithLevelParams___at_Lean_Elab_Term_toParserDescr_resolveParserName___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___spec__1___rarg(lean_object*);
 lean_object* l_Lean_Elab_Command_elabSyntax___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550____closed__1;
 lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_toParserDescr_resolveParserName___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_elabSyntaxAbbrev___closed__8;
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_inferMacroRulesAltKind___spec__2___boxed(lean_object*, lean_object*);
@@ -663,6 +664,7 @@ lean_object* l_Lean_Elab_Term_withAutoBoundImplicit___rarg(lean_object*, lean_ob
 lean_object* l_Lean_Elab_Term_toParserDescr_processSepBy(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_inferMacroRulesAltKind___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_pushInfoTree___at_Lean_Elab_Term_toParserDescr_resolveParserName___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2;
 lean_object* l_Lean_Elab_Term_toParserDescr_process_match__1___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@@ -14072,91 +14074,164 @@ lean_dec(x_1);
 return x_4;
 }
 }
+static lean_object* _init_l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("catBehaviorBoth");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__7;
+x_2 = l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
 lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; 
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; 
 x_5 = lean_unsigned_to_nat(1u);
 x_6 = l_Lean_Syntax_getArg(x_1, x_5);
 x_7 = l_Lean_Syntax_getId(x_6);
 lean_dec(x_6);
-x_8 = l_Subarray_forInUnsafe_loop___at___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___spec__1___closed__3;
+x_8 = lean_unsigned_to_nat(2u);
+x_9 = l_Lean_Syntax_getArg(x_1, x_8);
+x_10 = l_Lean_Syntax_isNone(x_9);
+x_11 = l_Subarray_forInUnsafe_loop___at___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___spec__1___closed__3;
 lean_inc(x_7);
-x_9 = lean_name_append_after(x_7, x_8);
-x_10 = lean_st_ref_get(x_3, x_4);
-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);
-lean_dec(x_11);
-x_14 = 0;
-lean_inc(x_7);
-x_15 = l_Lean_Parser_registerParserCategory(x_13, x_9, x_7, x_14, x_12);
-if (lean_obj_tag(x_15) == 0)
+x_12 = lean_name_append_after(x_7, x_11);
+x_13 = lean_st_ref_get(x_3, x_4);
+if (x_10 == 0)
 {
-lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
-x_16 = lean_ctor_get(x_15, 0);
-lean_inc(x_16);
-x_17 = lean_ctor_get(x_15, 1);
+lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; 
+x_40 = lean_unsigned_to_nat(3u);
+x_41 = l_Lean_Syntax_getArg(x_9, x_40);
+lean_dec(x_9);
+x_42 = l_Lean_Syntax_getKind(x_41);
+x_43 = l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2;
+x_44 = lean_name_eq(x_42, x_43);
+lean_dec(x_42);
+if (x_44 == 0)
+{
+lean_object* x_45; lean_object* x_46; uint8_t x_47; 
+x_45 = lean_ctor_get(x_13, 0);
+lean_inc(x_45);
+x_46 = lean_ctor_get(x_13, 1);
+lean_inc(x_46);
+lean_dec(x_13);
+x_47 = 1;
+x_14 = x_47;
+x_15 = x_45;
+x_16 = x_46;
+goto block_39;
+}
+else
+{
+lean_object* x_48; lean_object* x_49; uint8_t x_50; 
+x_48 = lean_ctor_get(x_13, 0);
+lean_inc(x_48);
+x_49 = lean_ctor_get(x_13, 1);
+lean_inc(x_49);
+lean_dec(x_13);
+x_50 = 2;
+x_14 = x_50;
+x_15 = x_48;
+x_16 = x_49;
+goto block_39;
+}
+}
+else
+{
+lean_object* x_51; lean_object* x_52; uint8_t x_53; 
+lean_dec(x_9);
+x_51 = lean_ctor_get(x_13, 0);
+lean_inc(x_51);
+x_52 = lean_ctor_get(x_13, 1);
+lean_inc(x_52);
+lean_dec(x_13);
+x_53 = 0;
+x_14 = x_53;
+x_15 = x_51;
+x_16 = x_52;
+goto block_39;
+}
+block_39:
+{
+lean_object* x_17; lean_object* x_18; 
+x_17 = lean_ctor_get(x_15, 0);
 lean_inc(x_17);
 lean_dec(x_15);
-x_18 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_16, x_2, x_3, x_17);
-x_19 = lean_ctor_get(x_18, 1);
+lean_inc(x_7);
+x_18 = l_Lean_Parser_registerParserCategory(x_17, x_12, x_7, x_14, x_16);
+if (lean_obj_tag(x_18) == 0)
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_19 = lean_ctor_get(x_18, 0);
 lean_inc(x_19);
+x_20 = lean_ctor_get(x_18, 1);
+lean_inc(x_20);
 lean_dec(x_18);
-x_20 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser(x_7, x_2, x_3, x_19);
-return x_20;
+x_21 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_19, x_2, x_3, x_20);
+x_22 = lean_ctor_get(x_21, 1);
+lean_inc(x_22);
+lean_dec(x_21);
+x_23 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser(x_7, x_2, x_3, x_22);
+return x_23;
 }
 else
 {
-uint8_t x_21; 
+uint8_t x_24; 
 lean_dec(x_7);
 lean_dec(x_3);
-x_21 = !lean_is_exclusive(x_15);
-if (x_21 == 0)
+x_24 = !lean_is_exclusive(x_18);
+if (x_24 == 0)
 {
-lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
-x_22 = lean_ctor_get(x_15, 0);
-x_23 = lean_ctor_get(x_2, 6);
-lean_inc(x_23);
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
+x_25 = lean_ctor_get(x_18, 0);
+x_26 = lean_ctor_get(x_2, 6);
+lean_inc(x_26);
 lean_dec(x_2);
-x_24 = lean_io_error_to_string(x_22);
-x_25 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_25, 0, x_24);
-x_26 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_26, 0, x_25);
-x_27 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_27, 0, x_23);
-lean_ctor_set(x_27, 1, x_26);
-lean_ctor_set(x_15, 0, x_27);
-return x_15;
+x_27 = lean_io_error_to_string(x_25);
+x_28 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_28, 0, x_27);
+x_29 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_29, 0, x_28);
+x_30 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_30, 0, x_26);
+lean_ctor_set(x_30, 1, x_29);
+lean_ctor_set(x_18, 0, x_30);
+return x_18;
 }
 else
 {
-lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; 
-x_28 = lean_ctor_get(x_15, 0);
-x_29 = lean_ctor_get(x_15, 1);
-lean_inc(x_29);
-lean_inc(x_28);
-lean_dec(x_15);
-x_30 = lean_ctor_get(x_2, 6);
-lean_inc(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; 
+x_31 = lean_ctor_get(x_18, 0);
+x_32 = lean_ctor_get(x_18, 1);
+lean_inc(x_32);
+lean_inc(x_31);
+lean_dec(x_18);
+x_33 = lean_ctor_get(x_2, 6);
+lean_inc(x_33);
 lean_dec(x_2);
-x_31 = lean_io_error_to_string(x_28);
-x_32 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_32, 0, x_31);
-x_33 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_33, 0, x_32);
-x_34 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_34, 0, x_30);
-lean_ctor_set(x_34, 1, x_33);
-x_35 = lean_alloc_ctor(1, 2, 0);
+x_34 = lean_io_error_to_string(x_31);
+x_35 = lean_alloc_ctor(2, 1, 0);
 lean_ctor_set(x_35, 0, x_34);
-lean_ctor_set(x_35, 1, x_29);
-return x_35;
+x_36 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_36, 0, x_35);
+x_37 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_37, 0, x_33);
+lean_ctor_set(x_37, 1, x_36);
+x_38 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_38, 0, x_37);
+lean_ctor_set(x_38, 1, x_32);
+return x_38;
+}
 }
 }
 }
@@ -20208,7 +20283,7 @@ lean_dec(x_2);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550____closed__1() {
+static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -20218,11 +20293,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550_(lean_object* x_1) {
+lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550____closed__1;
+x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567____closed__1;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }
@@ -20750,6 +20825,10 @@ l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___c
 lean_mark_persistent(l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__90);
 l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__91 = _init_l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__91();
 lean_mark_persistent(l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__91);
+l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1 = _init_l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1();
+lean_mark_persistent(l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1);
+l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2 = _init_l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2();
+lean_mark_persistent(l_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2);
 l___regBuiltin_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1 = _init_l___regBuiltin_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1);
 l___regBuiltin_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2 = _init_l___regBuiltin_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2();
@@ -20907,9 +20986,9 @@ l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__5 = _init_l_
 lean_mark_persistent(l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__5);
 l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__6 = _init_l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__6();
 lean_mark_persistent(l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__6);
-l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550____closed__1();
-lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550____closed__1);
-res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5550_(lean_io_mk_world());
+l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567____closed__1();
+lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567____closed__1);
+res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_5567_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));

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

@@ -15,6 +15,7 @@ extern "C" {
 #endif
 lean_object* l_List_reverse___rarg(lean_object*);
 lean_object* l_Lean_stringToMessageData(lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjections_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__13;
 static lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___closed__4;
@@ -23,29 +24,40 @@ lean_object* l_Lean_Elab_Tactic_withMainContext___rarg(lean_object*, lean_object
 static lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___closed__2;
 lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__6;
+lean_object* l_Lean_Meta_injections(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___closed__1;
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__7;
 lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_getInjectionNewIds(lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjections___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection(lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__10;
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__3;
+static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__4;
+static lean_object* l_Lean_Elab_Tactic_evalInjections___rarg___closed__1;
 lean_object* l_List_mapTRAux___at___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___spec__1(lean_object*, lean_object*);
+static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__2;
 lean_object* l_Lean_Elab_Tactic_getNameOfIdent_x27(lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__5;
 lean_object* lean_array_to_list(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalInjection_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjections(lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__12;
 lean_object* l_Lean_Elab_Tactic_evalInjection___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__3;
+static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__5;
 extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
 static lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___closed__6;
+static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__1;
 lean_object* l_Lean_Meta_throwTacticEx___rarg(lean_object*, lean_object*, lean_object*, 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*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalInjection_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjections___rarg(lean_object*, lean_object*, lean_object*, lean_object*, 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*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjections_match__1(lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__9;
 uint8_t l_Lean_Syntax_isNone(lean_object*);
 static lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___closed__5;
@@ -57,9 +69,11 @@ lean_object* l_Lean_Elab_Tactic_replaceMainGoal(lean_object*, lean_object*, lean
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__1;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds___closed__3;
+lean_object* l_Lean_Elab_Tactic_evalInjections(lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__11;
-lean_object* l_Lean_Meta_injection(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_injection(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_List_isEmpty___rarg(lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInjections___boxed(lean_object*);
 lean_object* l_List_mapTRAux___at___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_getInjectionNewIds___spec__1(lean_object*, lean_object*);
 lean_object* l_List_mapTRAux___at___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_getInjectionNewIds___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
@@ -340,110 +354,92 @@ lean_inc(x_3);
 x_12 = l_Lean_Elab_Tactic_getMainGoal(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
 if (lean_obj_tag(x_12) == 0)
 {
-lean_object* x_13; lean_object* x_14; uint8_t x_15; uint8_t x_64; 
+lean_object* x_13; lean_object* x_14; lean_object* x_15; 
 x_13 = lean_ctor_get(x_12, 0);
 lean_inc(x_13);
 x_14 = lean_ctor_get(x_12, 1);
 lean_inc(x_14);
 lean_dec(x_12);
-x_64 = l_List_isEmpty___rarg(x_2);
-if (x_64 == 0)
-{
-uint8_t x_65; 
-x_65 = 1;
-x_15 = x_65;
-goto block_63;
-}
-else
-{
-uint8_t x_66; 
-x_66 = 0;
-x_15 = x_66;
-goto block_63;
-}
-block_63:
-{
-lean_object* x_16; 
 lean_inc(x_10);
 lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_7);
 lean_inc(x_2);
 lean_inc(x_13);
-x_16 = l_Lean_Meta_injection(x_13, x_1, x_2, x_15, x_7, x_8, x_9, x_10, x_14);
+x_15 = l_Lean_Meta_injection(x_13, x_1, x_2, x_7, x_8, x_9, x_10, x_14);
+if (lean_obj_tag(x_15) == 0)
+{
+lean_object* x_16; 
+x_16 = lean_ctor_get(x_15, 0);
+lean_inc(x_16);
 if (lean_obj_tag(x_16) == 0)
 {
-lean_object* x_17; 
-x_17 = lean_ctor_get(x_16, 0);
+lean_object* x_17; lean_object* x_18; 
+x_17 = lean_ctor_get(x_15, 1);
 lean_inc(x_17);
-if (lean_obj_tag(x_17) == 0)
-{
-lean_object* x_18; lean_object* x_19; 
-x_18 = lean_ctor_get(x_16, 1);
-lean_inc(x_18);
-lean_dec(x_16);
+lean_dec(x_15);
 lean_inc(x_8);
-x_19 = l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds(x_13, x_2, x_7, x_8, x_9, x_10, x_18);
-if (lean_obj_tag(x_19) == 0)
+x_18 = l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds(x_13, x_2, x_7, x_8, x_9, x_10, x_17);
+if (lean_obj_tag(x_18) == 0)
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-x_20 = lean_ctor_get(x_19, 1);
-lean_inc(x_20);
-lean_dec(x_19);
-x_21 = lean_box(0);
-x_22 = l_Lean_Elab_Tactic_replaceMainGoal(x_21, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_20);
-if (lean_obj_tag(x_22) == 0)
+lean_object* x_19; lean_object* x_20; lean_object* x_21; 
+x_19 = lean_ctor_get(x_18, 1);
+lean_inc(x_19);
+lean_dec(x_18);
+x_20 = lean_box(0);
+x_21 = l_Lean_Elab_Tactic_replaceMainGoal(x_20, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_19);
+if (lean_obj_tag(x_21) == 0)
 {
-uint8_t x_23; 
-x_23 = !lean_is_exclusive(x_22);
-if (x_23 == 0)
+uint8_t x_22; 
+x_22 = !lean_is_exclusive(x_21);
+if (x_22 == 0)
 {
-lean_object* x_24; lean_object* x_25; 
-x_24 = lean_ctor_get(x_22, 0);
-lean_dec(x_24);
-x_25 = lean_box(0);
-lean_ctor_set(x_22, 0, x_25);
-return x_22;
+lean_object* x_23; lean_object* x_24; 
+x_23 = lean_ctor_get(x_21, 0);
+lean_dec(x_23);
+x_24 = lean_box(0);
+lean_ctor_set(x_21, 0, x_24);
+return x_21;
 }
 else
 {
-lean_object* x_26; lean_object* x_27; lean_object* x_28; 
-x_26 = lean_ctor_get(x_22, 1);
-lean_inc(x_26);
-lean_dec(x_22);
-x_27 = lean_box(0);
-x_28 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_28, 0, x_27);
-lean_ctor_set(x_28, 1, x_26);
-return x_28;
+lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_25 = lean_ctor_get(x_21, 1);
+lean_inc(x_25);
+lean_dec(x_21);
+x_26 = lean_box(0);
+x_27 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_27, 0, x_26);
+lean_ctor_set(x_27, 1, x_25);
+return x_27;
 }
 }
 else
 {
-uint8_t x_29; 
-x_29 = !lean_is_exclusive(x_22);
-if (x_29 == 0)
+uint8_t x_28; 
+x_28 = !lean_is_exclusive(x_21);
+if (x_28 == 0)
 {
-return x_22;
+return x_21;
 }
 else
 {
-lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_22, 0);
-x_31 = lean_ctor_get(x_22, 1);
-lean_inc(x_31);
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_21, 0);
+x_30 = lean_ctor_get(x_21, 1);
 lean_inc(x_30);
-lean_dec(x_22);
-x_32 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_32, 0, x_30);
-lean_ctor_set(x_32, 1, x_31);
-return x_32;
+lean_inc(x_29);
+lean_dec(x_21);
+x_31 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_31, 0, x_29);
+lean_ctor_set(x_31, 1, x_30);
+return x_31;
 }
 }
 }
 else
 {
-uint8_t x_33; 
+uint8_t x_32; 
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
@@ -452,104 +448,104 @@ lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
-x_33 = !lean_is_exclusive(x_19);
-if (x_33 == 0)
+x_32 = !lean_is_exclusive(x_18);
+if (x_32 == 0)
 {
-return x_19;
+return x_18;
 }
 else
 {
-lean_object* x_34; lean_object* x_35; lean_object* x_36; 
-x_34 = lean_ctor_get(x_19, 0);
-x_35 = lean_ctor_get(x_19, 1);
-lean_inc(x_35);
+lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+x_33 = lean_ctor_get(x_18, 0);
+x_34 = lean_ctor_get(x_18, 1);
 lean_inc(x_34);
-lean_dec(x_19);
-x_36 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_36, 0, x_34);
-lean_ctor_set(x_36, 1, x_35);
-return x_36;
+lean_inc(x_33);
+lean_dec(x_18);
+x_35 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_35, 0, x_33);
+lean_ctor_set(x_35, 1, x_34);
+return x_35;
 }
 }
 }
 else
 {
-lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; 
+lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
 lean_dec(x_2);
-x_37 = lean_ctor_get(x_16, 1);
+x_36 = lean_ctor_get(x_15, 1);
+lean_inc(x_36);
+lean_dec(x_15);
+x_37 = lean_ctor_get(x_16, 0);
 lean_inc(x_37);
-lean_dec(x_16);
-x_38 = lean_ctor_get(x_17, 0);
+x_38 = lean_ctor_get(x_16, 2);
 lean_inc(x_38);
-x_39 = lean_ctor_get(x_17, 2);
-lean_inc(x_39);
-lean_dec(x_17);
+lean_dec(x_16);
 lean_inc(x_8);
-x_40 = l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds(x_13, x_39, x_7, x_8, x_9, x_10, x_37);
-if (lean_obj_tag(x_40) == 0)
+x_39 = l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds(x_13, x_38, x_7, x_8, x_9, x_10, x_36);
+if (lean_obj_tag(x_39) == 0)
 {
-lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; 
-x_41 = lean_ctor_get(x_40, 1);
-lean_inc(x_41);
-lean_dec(x_40);
-x_42 = lean_box(0);
-x_43 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_43, 0, x_38);
-lean_ctor_set(x_43, 1, x_42);
-x_44 = l_Lean_Elab_Tactic_replaceMainGoal(x_43, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_41);
-if (lean_obj_tag(x_44) == 0)
+lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_40 = lean_ctor_get(x_39, 1);
+lean_inc(x_40);
+lean_dec(x_39);
+x_41 = lean_box(0);
+x_42 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_42, 0, x_37);
+lean_ctor_set(x_42, 1, x_41);
+x_43 = l_Lean_Elab_Tactic_replaceMainGoal(x_42, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_40);
+if (lean_obj_tag(x_43) == 0)
 {
-uint8_t x_45; 
-x_45 = !lean_is_exclusive(x_44);
-if (x_45 == 0)
+uint8_t x_44; 
+x_44 = !lean_is_exclusive(x_43);
+if (x_44 == 0)
 {
-lean_object* x_46; lean_object* x_47; 
-x_46 = lean_ctor_get(x_44, 0);
-lean_dec(x_46);
-x_47 = lean_box(0);
-lean_ctor_set(x_44, 0, x_47);
-return x_44;
+lean_object* x_45; lean_object* x_46; 
+x_45 = lean_ctor_get(x_43, 0);
+lean_dec(x_45);
+x_46 = lean_box(0);
+lean_ctor_set(x_43, 0, x_46);
+return x_43;
 }
 else
 {
-lean_object* x_48; lean_object* x_49; lean_object* x_50; 
-x_48 = lean_ctor_get(x_44, 1);
-lean_inc(x_48);
-lean_dec(x_44);
-x_49 = lean_box(0);
-x_50 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_50, 0, x_49);
-lean_ctor_set(x_50, 1, x_48);
-return x_50;
+lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_47 = lean_ctor_get(x_43, 1);
+lean_inc(x_47);
+lean_dec(x_43);
+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);
+return x_49;
 }
 }
 else
 {
-uint8_t x_51; 
-x_51 = !lean_is_exclusive(x_44);
-if (x_51 == 0)
+uint8_t x_50; 
+x_50 = !lean_is_exclusive(x_43);
+if (x_50 == 0)
 {
-return x_44;
+return x_43;
 }
 else
 {
-lean_object* x_52; lean_object* x_53; lean_object* x_54; 
-x_52 = lean_ctor_get(x_44, 0);
-x_53 = lean_ctor_get(x_44, 1);
-lean_inc(x_53);
+lean_object* x_51; lean_object* x_52; lean_object* x_53; 
+x_51 = lean_ctor_get(x_43, 0);
+x_52 = lean_ctor_get(x_43, 1);
 lean_inc(x_52);
-lean_dec(x_44);
-x_54 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_54, 0, x_52);
-lean_ctor_set(x_54, 1, x_53);
-return x_54;
+lean_inc(x_51);
+lean_dec(x_43);
+x_53 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_53, 0, x_51);
+lean_ctor_set(x_53, 1, x_52);
+return x_53;
 }
 }
 }
 else
 {
-uint8_t x_55; 
-lean_dec(x_38);
+uint8_t x_54; 
+lean_dec(x_37);
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
@@ -558,30 +554,30 @@ lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
-x_55 = !lean_is_exclusive(x_40);
-if (x_55 == 0)
+x_54 = !lean_is_exclusive(x_39);
+if (x_54 == 0)
 {
-return x_40;
+return x_39;
 }
 else
 {
-lean_object* x_56; lean_object* x_57; lean_object* x_58; 
-x_56 = lean_ctor_get(x_40, 0);
-x_57 = lean_ctor_get(x_40, 1);
-lean_inc(x_57);
+lean_object* x_55; lean_object* x_56; lean_object* x_57; 
+x_55 = lean_ctor_get(x_39, 0);
+x_56 = lean_ctor_get(x_39, 1);
 lean_inc(x_56);
-lean_dec(x_40);
-x_58 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_58, 0, x_56);
-lean_ctor_set(x_58, 1, x_57);
-return x_58;
+lean_inc(x_55);
+lean_dec(x_39);
+x_57 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_57, 0, x_55);
+lean_ctor_set(x_57, 1, x_56);
+return x_57;
 }
 }
 }
 }
 else
 {
-uint8_t x_59; 
+uint8_t x_58; 
 lean_dec(x_13);
 lean_dec(x_10);
 lean_dec(x_9);
@@ -592,30 +588,29 @@ lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-x_59 = !lean_is_exclusive(x_16);
-if (x_59 == 0)
+x_58 = !lean_is_exclusive(x_15);
+if (x_58 == 0)
 {
-return x_16;
+return x_15;
 }
 else
 {
-lean_object* x_60; lean_object* x_61; lean_object* x_62; 
-x_60 = lean_ctor_get(x_16, 0);
-x_61 = lean_ctor_get(x_16, 1);
-lean_inc(x_61);
+lean_object* x_59; lean_object* x_60; lean_object* x_61; 
+x_59 = lean_ctor_get(x_15, 0);
+x_60 = lean_ctor_get(x_15, 1);
 lean_inc(x_60);
-lean_dec(x_16);
-x_62 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_62, 0, x_60);
-lean_ctor_set(x_62, 1, x_61);
-return x_62;
-}
+lean_inc(x_59);
+lean_dec(x_15);
+x_61 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_61, 0, x_59);
+lean_ctor_set(x_61, 1, x_60);
+return x_61;
 }
 }
 }
 else
 {
-uint8_t x_67; 
+uint8_t x_62; 
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
@@ -626,23 +621,23 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_67 = !lean_is_exclusive(x_12);
-if (x_67 == 0)
+x_62 = !lean_is_exclusive(x_12);
+if (x_62 == 0)
 {
 return x_12;
 }
 else
 {
-lean_object* x_68; lean_object* x_69; lean_object* x_70; 
-x_68 = lean_ctor_get(x_12, 0);
-x_69 = lean_ctor_get(x_12, 1);
-lean_inc(x_69);
-lean_inc(x_68);
+lean_object* x_63; lean_object* x_64; lean_object* x_65; 
+x_63 = lean_ctor_get(x_12, 0);
+x_64 = lean_ctor_get(x_12, 1);
+lean_inc(x_64);
+lean_inc(x_63);
 lean_dec(x_12);
-x_70 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_70, 0, x_68);
-lean_ctor_set(x_70, 1, x_69);
-return x_70;
+x_65 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_65, 0, x_63);
+lean_ctor_set(x_65, 1, x_64);
+return x_65;
 }
 }
 }
@@ -851,6 +846,343 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
 return x_6;
 }
 }
+lean_object* l_Lean_Elab_Tactic_evalInjections_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_3);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_2, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_3, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjections_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjections_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjections___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; 
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+lean_inc(x_2);
+lean_inc(x_1);
+x_10 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+if (lean_obj_tag(x_10) == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+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_unsigned_to_nat(5u);
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_inc(x_5);
+x_14 = l_Lean_Meta_injections(x_11, x_13, x_5, x_6, x_7, x_8, x_12);
+if (lean_obj_tag(x_14) == 0)
+{
+lean_object* x_15; 
+x_15 = lean_ctor_get(x_14, 0);
+lean_inc(x_15);
+if (lean_obj_tag(x_15) == 0)
+{
+lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_16 = lean_ctor_get(x_14, 1);
+lean_inc(x_16);
+lean_dec(x_14);
+x_17 = lean_box(0);
+x_18 = l_Lean_Elab_Tactic_replaceMainGoal(x_17, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_16);
+if (lean_obj_tag(x_18) == 0)
+{
+uint8_t x_19; 
+x_19 = !lean_is_exclusive(x_18);
+if (x_19 == 0)
+{
+lean_object* x_20; lean_object* x_21; 
+x_20 = lean_ctor_get(x_18, 0);
+lean_dec(x_20);
+x_21 = lean_box(0);
+lean_ctor_set(x_18, 0, x_21);
+return x_18;
+}
+else
+{
+lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_22 = lean_ctor_get(x_18, 1);
+lean_inc(x_22);
+lean_dec(x_18);
+x_23 = lean_box(0);
+x_24 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_24, 0, x_23);
+lean_ctor_set(x_24, 1, x_22);
+return x_24;
+}
+}
+else
+{
+uint8_t x_25; 
+x_25 = !lean_is_exclusive(x_18);
+if (x_25 == 0)
+{
+return x_18;
+}
+else
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = lean_ctor_get(x_18, 0);
+x_27 = lean_ctor_get(x_18, 1);
+lean_inc(x_27);
+lean_inc(x_26);
+lean_dec(x_18);
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_26);
+lean_ctor_set(x_28, 1, x_27);
+return x_28;
+}
+}
+}
+else
+{
+lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 
+x_29 = lean_ctor_get(x_14, 1);
+lean_inc(x_29);
+lean_dec(x_14);
+x_30 = lean_ctor_get(x_15, 0);
+lean_inc(x_30);
+lean_dec(x_15);
+x_31 = lean_box(0);
+x_32 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_32, 0, x_30);
+lean_ctor_set(x_32, 1, x_31);
+x_33 = l_Lean_Elab_Tactic_replaceMainGoal(x_32, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_29);
+if (lean_obj_tag(x_33) == 0)
+{
+uint8_t x_34; 
+x_34 = !lean_is_exclusive(x_33);
+if (x_34 == 0)
+{
+lean_object* x_35; lean_object* x_36; 
+x_35 = lean_ctor_get(x_33, 0);
+lean_dec(x_35);
+x_36 = lean_box(0);
+lean_ctor_set(x_33, 0, x_36);
+return x_33;
+}
+else
+{
+lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_37 = lean_ctor_get(x_33, 1);
+lean_inc(x_37);
+lean_dec(x_33);
+x_38 = lean_box(0);
+x_39 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_39, 0, x_38);
+lean_ctor_set(x_39, 1, x_37);
+return x_39;
+}
+}
+else
+{
+uint8_t x_40; 
+x_40 = !lean_is_exclusive(x_33);
+if (x_40 == 0)
+{
+return x_33;
+}
+else
+{
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_33, 0);
+x_42 = lean_ctor_get(x_33, 1);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_dec(x_33);
+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_8);
+lean_dec(x_7);
+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_44 = !lean_is_exclusive(x_14);
+if (x_44 == 0)
+{
+return x_14;
+}
+else
+{
+lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_45 = lean_ctor_get(x_14, 0);
+x_46 = lean_ctor_get(x_14, 1);
+lean_inc(x_46);
+lean_inc(x_45);
+lean_dec(x_14);
+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;
+}
+}
+}
+else
+{
+uint8_t x_48; 
+lean_dec(x_8);
+lean_dec(x_7);
+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_48 = !lean_is_exclusive(x_10);
+if (x_48 == 0)
+{
+return x_10;
+}
+else
+{
+lean_object* x_49; lean_object* x_50; lean_object* x_51; 
+x_49 = lean_ctor_get(x_10, 0);
+x_50 = lean_ctor_get(x_10, 1);
+lean_inc(x_50);
+lean_inc(x_49);
+lean_dec(x_10);
+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;
+}
+}
+}
+}
+static lean_object* _init_l_Lean_Elab_Tactic_evalInjections___rarg___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjections___rarg___lambda__1), 9, 0);
+return x_1;
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjections___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = l_Lean_Elab_Tactic_evalInjections___rarg___closed__1;
+x_11 = l_Lean_Elab_Tactic_withMainContext___rarg(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+return x_11;
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjections(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjections___rarg), 9, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Elab_Tactic_evalInjections___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Elab_Tactic_evalInjections(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("injections");
+return x_1;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__6;
+x_2 = l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("evalInjections");
+return x_1;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__10;
+x_2 = l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__3;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__5() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjections___boxed), 1, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjections(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
+x_3 = l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__2;
+x_4 = l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__4;
+x_5 = l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__5;
+x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
+return x_6;
+}
+}
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Meta_Tactic_Injection(lean_object*);
 lean_object* initialize_Lean_Elab_Tactic_ElabTerm(lean_object*);
@@ -909,6 +1241,21 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__13)
 res = l___regBuiltin_Lean_Elab_Tactic_evalInjection(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Elab_Tactic_evalInjections___rarg___closed__1 = _init_l_Lean_Elab_Tactic_evalInjections___rarg___closed__1();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalInjections___rarg___closed__1);
+l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__1);
+l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__2);
+l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__3);
+l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__4 = _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__4();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__4);
+l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__5 = _init_l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__5();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalInjections___closed__5);
+res = l___regBuiltin_Lean_Elab_Tactic_evalInjections(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Meta/Injective.c

@@ -182,7 +182,7 @@ lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremType
 lean_object* l_Lean_Meta_mkHEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_elimOptParam___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkFreshExprSyntheticOpaqueMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Meta_injection(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_injection(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_elimOptParam___closed__2;
@@ -3205,112 +3205,111 @@ return x_1;
 lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
-lean_object* x_9; uint8_t x_10; lean_object* x_11; 
+lean_object* x_9; lean_object* x_10; 
 x_9 = lean_box(0);
-x_10 = 1;
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
-x_11 = l_Lean_Meta_injection(x_2, x_3, x_9, x_10, x_4, x_5, x_6, x_7, x_8);
+x_10 = l_Lean_Meta_injection(x_2, x_3, x_9, x_4, x_5, x_6, x_7, x_8);
+if (lean_obj_tag(x_10) == 0)
+{
+lean_object* x_11; 
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
 if (lean_obj_tag(x_11) == 0)
 {
-lean_object* x_12; 
-x_12 = lean_ctor_get(x_11, 0);
-lean_inc(x_12);
-if (lean_obj_tag(x_12) == 0)
-{
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
 lean_dec(x_1);
-x_13 = lean_ctor_get(x_11, 1);
-lean_inc(x_13);
-lean_dec(x_11);
-x_14 = l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__1;
-x_15 = l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__5;
-x_16 = lean_panic_fn(x_14, x_15);
-x_17 = lean_apply_5(x_16, x_4, x_5, x_6, x_7, x_13);
-return x_17;
+x_12 = lean_ctor_get(x_10, 1);
+lean_inc(x_12);
+lean_dec(x_10);
+x_13 = l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__1;
+x_14 = l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__5;
+x_15 = lean_panic_fn(x_13, x_14);
+x_16 = lean_apply_5(x_15, x_4, x_5, x_6, x_7, x_12);
+return x_16;
 }
 else
 {
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_18 = lean_ctor_get(x_11, 1);
+lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+x_17 = lean_ctor_get(x_10, 1);
+lean_inc(x_17);
+lean_dec(x_10);
+x_18 = lean_ctor_get(x_11, 0);
 lean_inc(x_18);
 lean_dec(x_11);
-x_19 = lean_ctor_get(x_12, 0);
-lean_inc(x_19);
-lean_dec(x_12);
-x_20 = l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__6;
+x_19 = l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__6;
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
-x_21 = l_Lean_Meta_saturate(x_19, x_20, x_4, x_5, x_6, x_7, x_18);
-if (lean_obj_tag(x_21) == 0)
+x_20 = l_Lean_Meta_saturate(x_18, x_19, x_4, x_5, x_6, x_7, x_17);
+if (lean_obj_tag(x_20) == 0)
 {
-lean_object* x_22; lean_object* x_23; lean_object* x_24; 
-x_22 = lean_ctor_get(x_21, 0);
+lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_21 = lean_ctor_get(x_20, 0);
+lean_inc(x_21);
+x_22 = lean_ctor_get(x_20, 1);
 lean_inc(x_22);
-x_23 = lean_ctor_get(x_21, 1);
-lean_inc(x_23);
-lean_dec(x_21);
-x_24 = l_List_forM___at___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___spec__1(x_1, x_22, x_4, x_5, x_6, x_7, x_23);
-return x_24;
+lean_dec(x_20);
+x_23 = l_List_forM___at___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___spec__1(x_1, x_21, x_4, x_5, x_6, x_7, x_22);
+return x_23;
 }
 else
 {
-uint8_t x_25; 
+uint8_t x_24; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_1);
-x_25 = !lean_is_exclusive(x_21);
-if (x_25 == 0)
+x_24 = !lean_is_exclusive(x_20);
+if (x_24 == 0)
 {
-return x_21;
+return x_20;
 }
 else
 {
-lean_object* x_26; lean_object* x_27; lean_object* x_28; 
-x_26 = lean_ctor_get(x_21, 0);
-x_27 = lean_ctor_get(x_21, 1);
-lean_inc(x_27);
+lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_25 = lean_ctor_get(x_20, 0);
+x_26 = lean_ctor_get(x_20, 1);
 lean_inc(x_26);
-lean_dec(x_21);
-x_28 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_28, 0, x_26);
-lean_ctor_set(x_28, 1, x_27);
-return x_28;
+lean_inc(x_25);
+lean_dec(x_20);
+x_27 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_27, 0, x_25);
+lean_ctor_set(x_27, 1, x_26);
+return x_27;
 }
 }
 }
 }
 else
 {
-uint8_t x_29; 
+uint8_t x_28; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_1);
-x_29 = !lean_is_exclusive(x_11);
-if (x_29 == 0)
+x_28 = !lean_is_exclusive(x_10);
+if (x_28 == 0)
 {
-return x_11;
+return x_10;
 }
 else
 {
-lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_11, 0);
-x_31 = lean_ctor_get(x_11, 1);
-lean_inc(x_31);
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_10, 0);
+x_30 = lean_ctor_get(x_10, 1);
 lean_inc(x_30);
-lean_dec(x_11);
-x_32 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_32, 0, x_30);
-lean_ctor_set(x_32, 1, x_31);
-return x_32;
+lean_inc(x_29);
+lean_dec(x_10);
+x_31 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_31, 0, x_29);
+lean_ctor_set(x_31, 1, x_30);
+return x_31;
 }
 }
 }