Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean

/-!
# `casesm`, `cases_type`, `constructorm` tactics

These tactics implement repeated `cases` / `constructor` on anything satisfying a predicate.
-/

namespace Lean.MVarId

/--
Core tactic for `casesm` and `cases_type`. Calls `cases` on all fvars in `g` for which
`matcher ldecl.type` returns true.
* `recursive`: if true, it calls itself repeatedly on the resulting subgoals
* `allowSplit`: if false, it will skip any hypotheses where `cases` returns more than one subgoal.
* `throwOnNoMatch`: if true, then throws an error if no match is found
-/
partial def 
casesMatching: (Expr โ†’ MetaM Bool) โ†’
  (recursive : optParam Bool false) โ†’ optParam Bool true โ†’ optParam Bool !recursive โ†’ MVarId โ†’ MetaM (List MVarId)
casesMatching (
matcher: Expr โ†’ MetaM Bool
matcher : 
Expr: Type
Expr โ†’ 
MetaM: Type โ†’ Type
MetaM 
Bool: Type
Bool) (
recursive: optParam ?m.8 false
recursive := 
false: Bool
false) (
allowSplit: optParam ?m.12 true
allowSplit := 
true: Bool
true)
    (
throwOnNoMatch: optParam ?m.16 !recursive
throwOnNoMatch := !
recursive: optParam ?m.8 false
recursive) (
g: MVarId
g : 
MVarId: Type
MVarId) : 
MetaM: Type โ†’ Type
MetaM (
List: Type ?u.21 โ†’ Type ?u.21
List 
MVarId: Type
MVarId) := do
  let 
result: ?m.2330
result := 
(โ† go g): ?m.2327
(โ† 
go: MVarId โ†’ optParam (Array MVarId) #[] โ†’ MetaM (Array MVarId)
go
(โ† go g): ?m.2327
 
g: MVarId
g
(โ† go g): ?m.2327
).
toList: {ฮฑ : Type ?u.2331} โ†’ Array ฮฑ โ†’ List ฮฑ
toList
  if 
throwOnNoMatch: optParam Bool !recursive
throwOnNoMatch && 
result: ?m.2330
result == [
g: MVarId
g] then
    
throwError "no match": ?m.2443 ?m.2444
throwError
throwError "no match": ?m.2443 ?m.2444
 "no match"
  else
    return 
result: ?m.2330
result
  where
  /-- Auxiliary for `casesMatching`. Accumulates generated subgoals in `acc`. -/
  
go: (Expr โ†’ MetaM Bool) โ†’
  optParam Bool false โ†’ optParam Bool true โ†’ MVarId โ†’ optParam (Array MVarId) #[] โ†’ MetaM (Array MVarId)
go (
g: MVarId
g : 
MVarId: Type
MVarId) (
acc: optParam (Array MVarId) #[]
acc : 
Array: Type ?u.39 โ†’ Type ?u.39
Array 
MVarId: Type
MVarId := 
#[]: Array ?m.41
#[]) : 
MetaM: Type โ†’ Type
MetaM (
Array: Type ?u.48 โ†’ Type ?u.48
Array 
MVarId: Type
MVarId) :=
    
g: MVarId
g.
withContext: {n : Type โ†’ Type ?u.55} โ†’ [inst : MonadControlT MetaM n] โ†’ [inst : Monad n] โ†’ {ฮฑ : Type} โ†’ MVarId โ†’ n ฮฑ โ†’ n ฮฑ
withContext do
      for 
ldecl: ?m.273
ldecl in โ† 
getLCtx: {m : Type โ†’ Type} โ†’ [self : MonadLCtx m] โ†’ m LocalContext
getLCtx do
        if 
ldecl: ?m.273
ldecl.
isImplementationDetail: LocalDecl โ†’ Bool
isImplementationDetail then 
continue: ?m.388 ?m.390
continue
        if โ† 
matcher: Expr โ†’ MetaM Bool
matcher 
ldecl: ?m.273
ldecl.
type: LocalDecl โ†’ Expr
type then
          let mut 
acc: ?m.704
acc := 
acc: optParam (Array MVarId) #[]
acc
          let 
subgoals: ?m.711
subgoals โ† if 
allowSplit: optParam Bool true
allowSplit then
            
g: MVarId
g.
cases: MVarId โ†’ FVarId โ†’ optParam (Array Meta.AltVarNames) #[] โ†’ MetaM (Array Meta.CasesSubgoal)
cases 
ldecl: ?m.273
ldecl.
fvarId: LocalDecl โ†’ FVarId
fvarId
          else
            let 
s: ?m.915
s โ† 
saveState: {s : outParam Type} โ†’ {m : Type โ†’ Type} โ†’ [self : MonadBacktrack s m] โ†’ m s
saveState
            let 
subgoals: ?m.973
subgoals โ† 
g: MVarId
g.
cases: MVarId โ†’ FVarId โ†’ optParam (Array Meta.AltVarNames) #[] โ†’ MetaM (Array Meta.CasesSubgoal)
cases 
ldecl: ?m.273
ldecl.
fvarId: LocalDecl โ†’ FVarId
fvarId
            if 
subgoals: ?m.973
subgoals.
size: {ฮฑ : Type ?u.976} โ†’ Array ฮฑ โ†’ Nat
size > 
1: ?m.981
1 then
              
s: ?m.915
s.
restore: Meta.SavedState โ†’ MetaM Unit
restore
              
continue: ?m.1067 ?m.1069
continue
            else
              
pure: {f : Type ?u.1149 โ†’ Type ?u.1148} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.1149} โ†’ ฮฑ โ†’ f ฮฑ
pure 
subgoals: ?m.973
subgoals
          for 
subgoal: ?m.1302
subgoal in 
subgoals: ?m.715 acc
subgoals do
            if 
recursive: optParam Bool false
recursive then
              
acc: ?m.1423
acc โ† 
go: MVarId โ†’ optParam (Array MVarId) #[] โ†’ MetaM (Array MVarId)
go 
subgoal: ?m.1302
subgoal.
mvarId: Meta.InductionSubgoal โ†’ MVarId
mvarId 
acc: ?m.1308
acc
            else
              
acc: ?m.1542
acc := 
acc: ?m.1308
acc.
push: {ฮฑ : Type ?u.1543} โ†’ Array ฮฑ โ†’ ฮฑ โ†’ Array ฮฑ
push 
subgoal: ?m.1302
subgoal.
mvarId: Meta.InductionSubgoal โ†’ MVarId
mvarId
          return 
acc: ?m.1677
acc
      return (
acc: optParam (Array MVarId) #[]
acc.
push: {ฮฑ : Type ?u.2139} โ†’ Array ฮฑ โ†’ ฮฑ โ†’ Array ฮฑ
push 
g: MVarId
g)

def 
casesType: Array Name โ†’ optParam Bool false โ†’ optParam Bool true โ†’ MVarId โ†’ MetaM (List MVarId)
casesType (
heads: Array Name
heads : 
Array: Type ?u.7867 โ†’ Type ?u.7867
Array 
Name: Type
Name) (
recursive: optParam Bool false
recursive := 
false: Bool
false) (
allowSplit: optParam ?m.7875 true
allowSplit := 
true: Bool
true) :
     
MVarId: Type
MVarId โ†’ 
MetaM: Type โ†’ Type
MetaM (
List: Type ?u.7880 โ†’ Type ?u.7880
List 
MVarId: Type
MVarId) :=
  let 
matcher: (ty : ?m.7890) โ†’ ?m.7950 ty (?m.7949 ty)
matcher 
ty: ?m.7890
ty := 
pure: {f : Type ?u.7895 โ†’ Type ?u.7894} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.7895} โ†’ ฮฑ โ†’ f ฮฑ
pure <|
    if let 
.const: Name โ†’ List Level โ†’ Expr
.const 
n: Name
n .. := 
ty: ?m.7890
ty.
headBeta: Expr โ†’ Expr
headBeta.
getAppFn: Expr โ†’ Expr
getAppFn then 
heads: Array Name
heads.
contains: {ฮฑ : Type ?u.7995} โ†’ [inst : BEq ฮฑ] โ†’ Array ฮฑ โ†’ ฮฑ โ†’ Bool
contains 
n: Name
n else 
false: Bool
false
  
casesMatching: (Expr โ†’ MetaM Bool) โ†’
  (recursive : optParam Bool false) โ†’ optParam Bool true โ†’ optParam Bool !recursive โ†’ MVarId โ†’ MetaM (List MVarId)
casesMatching 
matcher: (ty : ?m.7890) โ†’ ?m.7950 ty (?m.7949 ty)
matcher 
recursive: optParam Bool false
recursive 
allowSplit: optParam Bool true
allowSplit

end Lean.MVarId

namespace Mathlib.Tactic
open Lean Meta Elab Tactic MVarId

/-- Elaborate a list of terms with holes into a list of patterns. -/
def 
elabPatterns: Array Term โ†’ TermElabM (Array AbstractMVarsResult)
elabPatterns (
pats: Array Term
pats : 
Array: Type ?u.8813 โ†’ Type ?u.8813
Array 
Term: Type
Term) : 
TermElabM: Type โ†’ Type
TermElabM (
Array: Type ?u.8816 โ†’ Type ?u.8816
Array 
AbstractMVarsResult: Type
AbstractMVarsResult) :=
  
withTheReader: (ฯ : Type ?u.8821) โ†’
  {m : Type ?u.8821 โ†’ Type ?u.8820} โ†’ [inst : MonadWithReaderOf ฯ m] โ†’ {ฮฑ : Type ?u.8821} โ†’ (ฯ โ†’ ฯ) โ†’ m ฮฑ โ†’ m ฮฑ
withTheReader 
Term.Context: Type
Term.Context (fun 
ctx: ?m.8838
ctx โ†ฆ { 
ctx: ?m.8838
ctx with ignoreTCFailures := 
true: Bool
true }) <|
  
Term.withoutErrToSorry: {m : Type โ†’ Type ?u.8842} โ†’ {ฮฑ : Type} โ†’ [inst : MonadFunctorT TermElabM m] โ†’ m ฮฑ โ†’ m ฮฑ
Term.withoutErrToSorry <|
  
pats: Array Term
pats.
mapM: {ฮฑ : Type ?u.8862} โ†’
  {ฮฒ : Type ?u.8861} โ†’ {m : Type ?u.8861 โ†’ Type ?u.8860} โ†’ [inst : Monad m] โ†’ (ฮฑ โ†’ m ฮฒ) โ†’ Array ฮฑ โ†’ m (Array ฮฒ)
mapM fun 
p: ?m.8896
p โ†ฆ 
Term.withoutModifyingElabMetaStateWithInfo: {ฮฑ : Type} โ†’ TermElabM ฮฑ โ†’ TermElabM ฮฑ
Term.withoutModifyingElabMetaStateWithInfo do
    
withRef: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadRef m] โ†’ {ฮฑ : Type} โ†’ Syntax โ†’ m ฮฑ โ†’ m ฮฑ
withRef 
p: ?m.8896
p <| 
abstractMVars: Expr โ†’ MetaM AbstractMVarsResult
abstractMVars 
(โ† Term.elabTerm p none): ?m.8980
(โ† 
Term.elabTerm: Syntax โ†’ Option Expr โ†’ optParam Bool true โ†’ optParam Bool true โ†’ TermElabM Expr
Term.elabTerm
(โ† Term.elabTerm p none): ?m.8980
 
p: ?m.8896
p
(โ† Term.elabTerm p none): ?m.8980
 
none: {ฮฑ : Type ?u.8969} โ†’ Option ฮฑ
none
(โ† Term.elabTerm p none): ?m.8980
)

/-- Returns true if any of the patterns match the expression. -/
def 
matchPatterns: Array AbstractMVarsResult โ†’ Expr โ†’ MetaM Bool
matchPatterns (
pats: Array AbstractMVarsResult
pats : 
Array: Type ?u.12726 โ†’ Type ?u.12726
Array 
AbstractMVarsResult: Type
AbstractMVarsResult) (
e: Expr
e : 
Expr: Type
Expr) : 
MetaM: Type โ†’ Type
MetaM 
Bool: Type
Bool := do
  let 
e: ?m.12828
e โ† 
instantiateMVars: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ Expr โ†’ m Expr
instantiateMVars 
e: Expr
e
  
pats: Array AbstractMVarsResult
pats.
anyM: {ฮฑ : Type ?u.12831} โ†’
  {m : Type โ†’ Type ?u.12830} โ†’
    [inst : Monad m] โ†’ (ฮฑ โ†’ m Bool) โ†’ (as : Array ฮฑ) โ†’ optParam Nat 0 โ†’ optParam Nat (Array.size as) โ†’ m Bool
anyM fun 
p: ?m.12864
p โ†ฆ return 
(โ† Conv.matchPattern? p e): ?m.12918
(โ† 
Conv.matchPattern?: AbstractMVarsResult โ†’ Expr โ†’ MetaM (Option (Expr ร— Array Expr))
Conv.matchPattern?
(โ† Conv.matchPattern? p e): ?m.12918
 
p: ?m.12864
p
(โ† Conv.matchPattern? p e): ?m.12918
 
e: ?m.12828
e
(โ† Conv.matchPattern? p e): ?m.12918
) matches 
some: {ฮฑ : Type ?u.12947} โ†’ ฮฑ โ†’ Option ฮฑ
some (_, #[])

/--
* `casesm p` applies the `cases` tactic to a hypothesis `h : type`
  if `type` matches the pattern `p`.
* `casesm p_1, ..., p_n` applies the `cases` tactic to a hypothesis `h : type`
  if `type` matches one of the given patterns.
* `casesm* p` is a more efficient and compact version of `ยท repeat casesm p`.
  It is more efficient because the pattern is compiled once.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.
```
casesm* _ โˆจ _, _ โˆง _
```
-/
elab (name := 
casesM: ParserDescr
casesM) "casesm" 
recursive: ?m.14335
recursive:"*"? 
ppSpace: Parser.Parser
ppSpace 
pats: ?m.14317
pats:
term: Parser.Category
term,+ : 
tactic: Parser.Category
tactic => do
  let 
pats: ?m.14534
pats โ† 
elabPatterns: Array Term โ†’ TermElabM (Array AbstractMVarsResult)
elabPatterns 
pats: ?m.14317
pats.
getElems: {k : SyntaxNodeKinds} โ†’ {sep : String} โ†’ Syntax.TSepArray k sep โ†’ TSyntaxArray k
getElems
  
liftMetaTactic: (MVarId โ†’ MetaM (List MVarId)) โ†’ TacticM Unit
liftMetaTactic (
casesMatching: (Expr โ†’ MetaM Bool) โ†’
  (recursive : optParam Bool false) โ†’ optParam Bool true โ†’ optParam Bool !recursive โ†’ MVarId โ†’ MetaM (List MVarId)
casesMatching (
matchPatterns: Array AbstractMVarsResult โ†’ Expr โ†’ MetaM Bool
matchPatterns 
pats: ?m.14534
pats) 
recursive: ?m.14335
recursive.
isSome: {ฮฑ : Type ?u.14563} โ†’ Option ฮฑ โ†’ Bool
isSome)

/-- Common implementation of `cases_type` and `cases_type!`. -/
def 
elabCasesType: Array Ident โ†’ optParam Bool false โ†’ optParam Bool true โ†’ TacticM Unit
elabCasesType (
heads: Array Ident
heads : 
Array: Type ?u.15948 โ†’ Type ?u.15948
Array 
Ident: Type
Ident)
    (
recursive: optParam ?m.15952 false
recursive := 
false: Bool
false) (
allowSplit: optParam ?m.15956 true
allowSplit := 
true: Bool
true) : 
TacticM: Type โ†’ Type
TacticM 
Unit: Type
Unit := do
  let 
heads: ?m.16733
heads โ† 
heads: Array Ident
heads.
mapM: {ฮฑ : Type ?u.16023} โ†’
  {ฮฒ : Type ?u.16022} โ†’ {m : Type ?u.16022 โ†’ Type ?u.16021} โ†’ [inst : Monad m] โ†’ (ฮฑ โ†’ m ฮฒ) โ†’ Array ฮฑ โ†’ m (Array ฮฒ)
mapM 
resolveGlobalConstNoOverloadWithInfo: {m : Type โ†’ Type} โ†’
  [inst : Monad m] โ†’
    [inst : MonadInfoTree m] โ†’
      [inst : MonadResolveName m] โ†’
        [inst : MonadEnv m] โ†’ [inst : MonadError m] โ†’ Syntax โ†’ optParam (Option Expr) none โ†’ m Name
resolveGlobalConstNoOverloadWithInfo
  
liftMetaTactic: (MVarId โ†’ MetaM (List MVarId)) โ†’ TacticM Unit
liftMetaTactic (
casesType: Array Name โ†’ optParam Bool false โ†’ optParam Bool true โ†’ MVarId โ†’ MetaM (List MVarId)
casesType 
heads: ?m.16733
heads 
recursive: optParam Bool false
recursive 
allowSplit: optParam Bool true
allowSplit)

/--
* `cases_type I` applies the `cases` tactic to a hypothesis `h : (I ...)`
* `cases_type I_1 ... I_n` applies the `cases` tactic to a hypothesis
  `h : (I_1 ...)` or ... or `h : (I_n ...)`
* `cases_type* I` is shorthand for `ยท repeat cases_type I`
* `cases_type! I` only applies `cases` if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current goal.
```
cases_type* Or And
```
-/
elab (name := 
casesType: ParserDescr
casesType) "cases_type" 
recursive: ?m.17868
recursive:"*"? 
ppSpace: Parser.Parser
ppSpace 
heads: ?m.17852
heads:(
colGt: optParam String "checkColGt" โ†’ Parser.Parser
colGt 
ident: Parser.Parser
ident)+ : 
tactic: Parser.Category
tactic =>
  
elabCasesType: Array Ident โ†’ optParam Bool false โ†’ optParam Bool true โ†’ TacticM Unit
elabCasesType 
heads: ?m.17852
heads 
recursive: ?m.17868
recursive.
isSome: {ฮฑ : Type ?u.17897} โ†’ Option ฮฑ โ†’ Bool
isSome 
true: Bool
true

@[inherit_doc 
casesType: ParserDescr
casesType]
elab (name := 
casesType!: ParserDescr
casesType!) "cases_type!" 
recursive: ?m.18812
recursive:"*"? 
ppSpace: Parser.Parser
ppSpace 
heads: ?m.18796
heads:(
colGt: optParam String "checkColGt" โ†’ Parser.Parser
colGt 
ident: Parser.Parser
ident)+ : 
tactic: Parser.Category
tactic =>
  
elabCasesType: Array Ident โ†’ optParam Bool false โ†’ optParam Bool true โ†’ TacticM Unit
elabCasesType 
heads: ?m.18796
heads 
recursive: ?m.18812
recursive.
isSome: {ฮฑ : Type ?u.18841} โ†’ Option ฮฑ โ†’ Bool
isSome 
false: Bool
false

/--
Core tactic for `constructorm`. Calls `constructor` on all subgoals for which
`matcher ldecl.type` returns true.
* `recursive`: if true, it calls itself repeatedly on the resulting subgoals
* `throwOnNoMatch`: if true, throws an error if no match is found
-/
partial def 
constructorMatching: MVarId โ†’ (Expr โ†’ MetaM Bool) โ†’ (recursive : optParam Bool false) โ†’ optParam Bool !recursive โ†’ MetaM (List MVarId)
constructorMatching (
g: MVarId
g : 
MVarId: Type
MVarId) (
matcher: Expr โ†’ MetaM Bool
matcher : 
Expr: Type
Expr โ†’ 
MetaM: Type โ†’ Type
MetaM 
Bool: Type
Bool)
    (
recursive: optParam ?m.19643 false
recursive := 
false: Bool
false) (
throwOnNoMatch: optParam ?m.19647 !recursive
throwOnNoMatch := !
recursive: optParam ?m.19643 false
recursive): 
MetaM: Type โ†’ Type
MetaM (
List: Type ?u.19650 โ†’ Type ?u.19650
List 
MVarId: Type
MVarId) := do
  let 
result: ?m.21087
result โ†
    (if 
recursive: optParam Bool false
recursive then (do
      let 
result: ?m.20755
result โ† 
go: MVarId โ†’ optParam (Array MVarId) #[] โ†’ MetaM (Array MVarId)
go 
g: MVarId
g
      
pure: {f : Type ?u.20758 โ†’ Type ?u.20757} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.20758} โ†’ ฮฑ โ†’ f ฮฑ
pure 
result: ?m.20755
result.
toList: {ฮฑ : Type ?u.20782} โ†’ Array ฮฑ โ†’ List ฮฑ
toList)
     else
      (
g: MVarId
g.
withContext: {n : Type โ†’ Type ?u.20798} โ†’ [inst : MonadControlT MetaM n] โ†’ [inst : Monad n] โ†’ {ฮฑ : Type} โ†’ MVarId โ†’ n ฮฑ โ†’ n ฮฑ
withContext do
          if โ† 
matcher: Expr โ†’ MetaM Bool
matcher 
(โ† g.getType): ?m.20897
(โ† 
g: MVarId
g
(โ† g.getType): ?m.20897
.
getType: MVarId โ†’ MetaM Expr
getType
(โ† g.getType): ?m.20897
) then 
g: MVarId
g.
constructor: MVarId โ†’
  optParam ApplyConfig { newGoals := ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true } โ†’
    MetaM (List MVarId)
constructor else 
pure: {f : Type ?u.21024 โ†’ Type ?u.21023} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.21024} โ†’ ฮฑ โ†’ f ฮฑ
pure [
g: MVarId
g]))
  if 
throwOnNoMatch: optParam Bool !recursive
throwOnNoMatch && [
g: MVarId
g] == 
result: ?m.21087
result then
    
throwError "no match": ?m.21167 ?m.21168
throwError
throwError "no match": ?m.21167 ?m.21168
 "no match"
  else
    return 
result: ?m.21087
result
where
  /-- Auxiliary for `constructorMatching`. Accumulates generated subgoals in `acc`. -/
  
go: (Expr โ†’ MetaM Bool) โ†’ MVarId โ†’ optParam (Array MVarId) #[] โ†’ MetaM (Array MVarId)
go (
g: MVarId
g : 
MVarId: Type
MVarId) (
acc: optParam (Array MVarId) #[]
acc : 
Array: Type ?u.19666 โ†’ Type ?u.19666
Array 
MVarId: Type
MVarId := 
#[]: Array ?m.19668
#[]) : 
MetaM: Type โ†’ Type
MetaM (
Array: Type ?u.19675 โ†’ Type ?u.19675
Array 
MVarId: Type
MVarId) :=
    
g: MVarId
g.
withContext: {n : Type โ†’ Type ?u.19682} โ†’ [inst : MonadControlT MetaM n] โ†’ [inst : Monad n] โ†’ {ฮฑ : Type} โ†’ MVarId โ†’ n ฮฑ โ†’ n ฮฑ
withContext do
      if โ† 
matcher: Expr โ†’ MetaM Bool
matcher 
(โ† g.getType): ?m.19796
(โ† 
g: MVarId
g
(โ† g.getType): ?m.19796
.
getType: MVarId โ†’ MetaM Expr
getType
(โ† g.getType): ?m.19796
) then
        let mut 
acc: ?m.20097
acc := 
acc: optParam (Array MVarId) #[]
acc
        for 
g': ?m.20091
g' in โ† 
g: MVarId
g.
constructor: MVarId โ†’
  optParam ApplyConfig { newGoals := ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true } โ†’
    MetaM (List MVarId)
constructor do
          
acc: ?m.20149
acc โ† 
go: MVarId โ†’ optParam (Array MVarId) #[] โ†’ MetaM (Array MVarId)
go 
g': ?m.20091
g' 
acc: ?m.20097
acc
        return 
acc: ?m.20332
acc
      return (
acc: optParam (Array MVarId) #[]
acc.
push: {ฮฑ : Type ?u.20520} โ†’ Array ฮฑ โ†’ ฮฑ โ†’ Array ฮฑ
push 
g: MVarId
g)

/--
* `constructorm p_1, ..., p_n` applies the `constructor` tactic to the main goal
  if `type` matches one of the given patterns.
* `constructorm* p` is a more efficient and compact version of `ยท repeat constructorm p`.
  It is more efficient because the pattern is compiled once.

Example: The following tactic proves any theorem like `True โˆง (True โˆจ True)` consisting of
and/or/true:
```
constructorm* _ โˆจ _, _ โˆง _, True
```
-/
elab (name := 
constructorM: ParserDescr
constructorM) "constructorm" 
recursive: ?m.24310
recursive:"*"? 
ppSpace: Parser.Parser
ppSpace 
pats: ?m.24292
pats:
term: Parser.Category
term,+ : 
tactic: Parser.Category
tactic => do
  let 
pats: ?m.24509
pats โ† 
elabPatterns: Array Term โ†’ TermElabM (Array AbstractMVarsResult)
elabPatterns 
pats: ?m.24292
pats.
getElems: {k : SyntaxNodeKinds} โ†’ {sep : String} โ†’ Syntax.TSepArray k sep โ†’ TSyntaxArray k
getElems
  
liftMetaTactic: (MVarId โ†’ MetaM (List MVarId)) โ†’ TacticM Unit
liftMetaTactic (
constructorMatching: MVarId โ†’ (Expr โ†’ MetaM Bool) โ†’ (recursive : optParam Bool false) โ†’ optParam Bool !recursive โ†’ MetaM (List MVarId)
constructorMatching ยท (
matchPatterns: Array AbstractMVarsResult โ†’ Expr โ†’ MetaM Bool
matchPatterns 
pats: ?m.24509
pats) 
recursive: ?m.24310
recursive.
isSome: {ฮฑ : Type ?u.24540} โ†’ Option ฮฑ โ†’ Bool
isSome)