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) 2021 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Arthur Paulino, AurΓ©lien Saue, Mario Carneiro
-/
import Std.Tactic.Simpa
import Mathlib.Lean.Expr

/-!
#

Generally useful tactics.

-/

open Lean.Elab.Tactic

namespace Lean

open Elab

/--
Return the modifiers of declaration `nm` with (optional) docstring `newDoc`.
Currently, recursive or partial definitions are not supported, and no attributes are provided.
-/
def 
toModifiers: Name β†’ optParam (Option String) none β†’ CoreM Modifiers
toModifiers (
nm: Name
nm : 
Name: Type
Name) (
newDoc: optParam (Option String) none
newDoc : 
Option: Type ?u.5 β†’ Type ?u.5
Option 
String: Type
String := 
none: {Ξ± : Type ?u.6} β†’ Option Ξ±
none) :
  
CoreM: Type β†’ Type
CoreM 
Modifiers: Type
Modifiers := do
  let 
env: ?m.81
env ← 
getEnv: {m : Type β†’ Type} β†’ [self : MonadEnv m] β†’ m Environment
getEnv
  let 
d: ?m.251
d ← 
getConstInfo: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadEnv m] β†’ [inst : MonadError m] β†’ Name β†’ m ConstantInfo
getConstInfo 
nm: Name
nm
  let 
mods: Modifiers
mods : 
Modifiers: Type
Modifiers :=
  { docString? := 
newDoc: optParam (Option String) none
newDoc
    visibility :=
    if 
isPrivateNameExport: Name β†’ Bool
isPrivateNameExport 
nm: Name
nm then
      
Visibility.private: Visibility
Visibility.private
    else if 
isProtected: Environment β†’ Name β†’ Bool
isProtected 
env: ?m.81
env 
nm: Name
nm then
      
Visibility.regular: Visibility
Visibility.regular
    else
      
Visibility.protected: Visibility
Visibility.protected
    isNoncomputable := if (
env: ?m.81
env.
find?: Environment β†’ Name β†’ Option ConstantInfo
find? $ 
nm: Name
nm.
mkStr: Name β†’ String β†’ Name
mkStr 
"_cstage1": String
"_cstage1").
isSome: {Ξ± : Type ?u.411} β†’ Option Ξ± β†’ Bool
isSome then 
false: Bool
false else 
true: Bool
true
    recKind := 
RecKind.default: RecKind
RecKind.default -- nonrec only matters for name resolution, so is irrelevant (?)
    isUnsafe := 
d: ?m.251
d.
isUnsafe: ConstantInfo β†’ Bool
isUnsafe
    attrs := 
#[]: Array ?m.480
#[] }
  return 
mods: Modifiers
mods

/--
Make a PreDefinition taking some metadata from declaration `nm`.
You can provide a new type, value and (optional) docstring, but the remaining information is taken
from `nm`.
Currently only implemented for definitions and theorems. Also see docstring of `toModifiers`
-/
def 
toPreDefinition: Name β†’ Name β†’ Expr β†’ Expr β†’ optParam (Option String) none β†’ CoreM PreDefinition
toPreDefinition (
nm: Name
nm 
newNm: Name
newNm : 
Name: Type
Name) (
newType: Expr
newType 
newValue: Expr
newValue : 
Expr: Type
Expr) (
newDoc: optParam (Option String) none
newDoc : 
Option: Type ?u.1670 β†’ Type ?u.1670
Option 
String: Type
String := 
none: {Ξ± : Type ?u.1671} β†’ Option Ξ±
none) :
  
CoreM: Type β†’ Type
CoreM 
PreDefinition: Type
PreDefinition := do
  let 
d: ?m.1880
d ← 
getConstInfo: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadEnv m] β†’ [inst : MonadError m] β†’ Name β†’ m ConstantInfo
getConstInfo 
nm: Name
nm
  let 
mods: ?m.1925
mods ← 
toModifiers: Name β†’ optParam (Option String) none β†’ CoreM Modifiers
toModifiers 
nm: Name
nm 
newDoc: optParam (Option String) none
newDoc
  let 
predef: PreDefinition
predef : 
PreDefinition: Type
PreDefinition :=
  { ref := 
Syntax.missing: Syntax
Syntax.missing
    kind := if 
d: ?m.1880
d.
isDef: ConstantInfo β†’ Bool
isDef then 
DefKind.def: DefKind
DefKind.def else 
DefKind.theorem: DefKind
DefKind.theorem
    levelParams := 
d: ?m.1880
d.
levelParams: ConstantInfo β†’ List Name
levelParams
    modifiers := 
mods: ?m.1925
mods
    declName := 
newNm: Name
newNm
    type := 
newType: Expr
newType
    value := 
newValue: Expr
newValue }
  return 
predef: PreDefinition
predef

/-- Make `nm` protected. -/
def 
setProtected: {m : Type β†’ Type} β†’ [inst : MonadEnv m] β†’ Name β†’ m Unit
setProtected {
m: Type β†’ Type
m : 
Type: Type 1
Type β†’ 
Type: Type 1
Type} [
MonadEnv: (Type β†’ Type) β†’ Type
MonadEnv 
m: Type β†’ Type
m] (
nm: Name
nm : 
Name: Type
Name) : 
m: Type β†’ Type
m 
Unit: Type
Unit :=
  
modifyEnv: {m : Type β†’ Type} β†’ [self : MonadEnv m] β†’ (Environment β†’ Environment) β†’ m Unit
modifyEnv (
addProtected: Environment β†’ Name β†’ Environment
addProtected Β· 
nm: Name
nm)

namespace Parser.Tactic

syntax 
withArgs: ParserDescr
withArgs := " with " (
colGt: optParam String "checkColGt" β†’ Parser
colGt 
ident: Parser
ident)+
syntax 
usingArg: ParserDescr
usingArg := " using " 
term: Category
term

/-- Extract the arguments from a `simpArgs` syntax as an array of syntaxes -/
def 
getSimpArgs: Syntax β†’ TacticM (Array Syntax)
getSimpArgs : 
Syntax: Type
Syntax β†’ 
TacticM: Type β†’ Type
TacticM (
Array: Type ?u.2719 β†’ Type ?u.2719
Array 
Syntax: Type
Syntax)
  | `(
simpArgs: ParserDescr
simpArgs| [$
args: ?m.2762
args,*]) => 
pure: {f : Type ?u.2772 β†’ Type ?u.2771} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.2772} β†’ Ξ± β†’ f Ξ±
pure 
args: ?m.2762
args.
getElems: {k : SyntaxNodeKinds} β†’ {sep : String} β†’ Syntax.TSepArray k sep β†’ TSyntaxArray k
getElems
  | _                      => 
Elab.throwUnsupportedSyntax: {m : Type ?u.2995 β†’ Type ?u.2994} β†’ {Ξ± : Type ?u.2995} β†’ [inst : MonadExceptOf Exception m] β†’ m Ξ±
Elab.throwUnsupportedSyntax

/-- Extract the arguments from a `dsimpArgs` syntax as an array of syntaxes -/
def 
getDSimpArgs: Syntax β†’ TacticM (Array Syntax)
getDSimpArgs : 
Syntax: Type
Syntax β†’ 
TacticM: Type β†’ Type
TacticM (
Array: Type ?u.3744 β†’ Type ?u.3744
Array 
Syntax: Type
Syntax)
  | `(
dsimpArgs: ParserDescr
dsimpArgs| [$
args: ?m.3787
args,*]) => 
pure: {f : Type ?u.3799 β†’ Type ?u.3798} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.3799} β†’ Ξ± β†’ f Ξ±
pure 
args: ?m.3787
args.
getElems: {k : SyntaxNodeKinds} β†’ {sep : String} β†’ Syntax.TSepArray k sep β†’ TSyntaxArray k
getElems
  | _                       => 
Elab.throwUnsupportedSyntax: {m : Type ?u.4022 β†’ Type ?u.4021} β†’ {Ξ± : Type ?u.4022} β†’ [inst : MonadExceptOf Exception m] β†’ m Ξ±
Elab.throwUnsupportedSyntax

/-- Extract the arguments from a `withArgs` syntax as an array of syntaxes -/
def 
getWithArgs: Syntax β†’ TacticM (Array Syntax)
getWithArgs : 
Syntax: Type
Syntax β†’ 
TacticM: Type β†’ Type
TacticM (
Array: Type ?u.4773 β†’ Type ?u.4773
Array 
Syntax: Type
Syntax)
  | `(
withArgs: ParserDescr
withArgs| with $
args: ?m.4808
args*) => 
pure: {f : Type ?u.4816 β†’ Type ?u.4815} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.4816} β†’ Ξ± β†’ f Ξ±
pure 
args: ?m.4808
args
  | _                        => 
Elab.throwUnsupportedSyntax: {m : Type ?u.5032 β†’ Type ?u.5031} β†’ {Ξ± : Type ?u.5032} β†’ [inst : MonadExceptOf Exception m] β†’ m Ξ±
Elab.throwUnsupportedSyntax

/-- Extract the argument from a `usingArg` syntax as a syntax term -/
def 
getUsingArg: Syntax β†’ TacticM Syntax
getUsingArg : 
Syntax: Type
Syntax β†’ 
TacticM: Type β†’ Type
TacticM 
Syntax: Type
Syntax
  | `(
usingArg: ParserDescr
usingArg| using $
e: ?m.5773
e) => 
pure: {f : Type ?u.5782 β†’ Type ?u.5781} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.5782} β†’ Ξ± β†’ f Ξ±
pure 
e: ?m.5773
e
  | _                     => 
Elab.throwUnsupportedSyntax: {m : Type ?u.5969 β†’ Type ?u.5968} β†’ {Ξ± : Type ?u.5969} β†’ [inst : MonadExceptOf Exception m] β†’ m Ξ±
Elab.throwUnsupportedSyntax

/--
`repeat1 tac` applies `tac` to main goal at least once. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.
-/
macro "repeat1 " 
seq: ?m.6725
seq:
tacticSeq: Parser
tacticSeq : 
tactic: Category
tactic => `(tactic| (($
seq: ?m.6725
seq); repeat $
seq: ?m.6725
seq))

end Parser.Tactic
end Lean

namespace Lean.Elab.Tactic

/-- Given a local context and an array of `FVarIds` assumed to be in that local context, remove all
implementation details. -/
def 
filterOutImplementationDetails: LocalContext β†’ Array FVarId β†’ Array FVarId
filterOutImplementationDetails (
lctx: LocalContext
lctx : 
LocalContext: Type
LocalContext) (
fvarIds: Array FVarId
fvarIds : 
Array: Type ?u.8696 β†’ Type ?u.8696
Array 
FVarId: Type
FVarId) : 
Array: Type ?u.8699 β†’ Type ?u.8699
Array 
FVarId: Type
FVarId :=
  
fvarIds: Array FVarId
fvarIds.
filter: {Ξ± : Type ?u.8703} β†’ (Ξ± β†’ Bool) β†’ (as : Array Ξ±) β†’ optParam Nat 0 β†’ optParam Nat (Array.size as) β†’ Array Ξ±
filter (fun 
fvar: ?m.8712
fvar => ! (
lctx: LocalContext
lctx.
fvarIdToDecl: LocalContext β†’ PersistentHashMap FVarId LocalDecl
fvarIdToDecl.
find!: {Ξ± : Type ?u.8715} β†’
  {Ξ² : Type ?u.8714} β†’ {x : BEq Ξ±} β†’ {x_1 : Hashable Ξ±} β†’ [inst : Inhabited Ξ²] β†’ PersistentHashMap Ξ± Ξ² β†’ Ξ± β†’ Ξ²
find! 
fvar: ?m.8712
fvar).
isImplementationDetail: LocalDecl β†’ Bool
isImplementationDetail)

/-- Elaborate syntax for an `FVarId` in the local context of the given goal. -/
def 
getFVarIdAt: MVarId β†’ Syntax β†’ TacticM FVarId
getFVarIdAt (
goal: MVarId
goal : 
MVarId: Type
MVarId) (
id: Syntax
id : 
Syntax: Type
Syntax) : 
TacticM: Type β†’ Type
TacticM 
FVarId: Type
FVarId := 
withRef: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadRef m] β†’ {Ξ± : Type} β†’ Syntax β†’ m Ξ± β†’ m Ξ±
withRef 
id: Syntax
id do
  -- use apply-like elaboration to suppress insertion of implicit arguments
  let 
e: ?m.9459
e ← 
goal: MVarId
goal.
withContext: {n : Type β†’ Type ?u.9169} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ MVarId β†’ n Ξ± β†’ n Ξ±
withContext do
    
elabTermForApply: Syntax β†’ optParam Bool true β†’ TacticM Expr
elabTermForApply 
id: Syntax
id (mayPostpone := 
false: Bool
false)
  match 
e: ?m.9459
e with
  | 
Expr.fvar: FVarId β†’ Expr
Expr.fvar 
fvarId: FVarId
fvarId => return 
fvarId: FVarId
fvarId
  | _                => throwError "unexpected term '{
e: ?m.9459
e}'; expected single reference to variable"

/-- Get the array of `FVarId`s in the local context of the given `goal`.

If `ids` is specified, elaborate them in the local context of the given goal to obtain the array of
`FVarId`s.

If `includeImplementationDetails` is `false` (the default), we filter out implementation details
(`implDecl`s and `auxDecl`s) from the resulting list of `FVarId`s. -/
def 
getFVarIdsAt: MVarId β†’ optParam (Option (Array Syntax)) none β†’ optParam Bool false β†’ TacticM (Array FVarId)
getFVarIdsAt (
goal: MVarId
goal : 
MVarId: Type
MVarId) (
ids: optParam (Option (Array Syntax)) none
ids : 
Option: Type ?u.12791 β†’ Type ?u.12791
Option (
Array: Type ?u.12792 β†’ Type ?u.12792
Array 
Syntax: Type
Syntax) := 
none: {Ξ± : Type ?u.12793} β†’ Option Ξ±
none)
    (
includeImplementationDetails: optParam Bool false
includeImplementationDetails : 
Bool: Type
Bool := 
false: Bool
false) : 
TacticM: Type β†’ Type
TacticM (
Array: Type ?u.12801 β†’ Type ?u.12801
Array 
FVarId: Type
FVarId) :=
  
goal: MVarId
goal.
withContext: {n : Type β†’ Type ?u.12809} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ MVarId β†’ n Ξ± β†’ n Ξ±
withContext do
    let 
lctx: ?m.13104
lctx := 
(← goal.getDecl): ?m.13101
(← 
goal: MVarId
goal
(← goal.getDecl): ?m.13101
.
getDecl: MVarId β†’ MetaM MetavarDecl
getDecl
(← goal.getDecl): ?m.13101
).
lctx: MetavarDecl β†’ LocalContext
lctx
    let 
fvarIds: ?m.13107
fvarIds ← match 
ids: optParam (Option (Array Syntax)) none
ids with
    | 
none: {Ξ± : Type ?u.13116} β†’ Option Ξ±
none => 
pure: {f : Type ?u.13161 β†’ Type ?u.13160} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.13161} β†’ Ξ± β†’ f Ξ±
pure
pure lctx.getFVarIds: TacticM (?m.13111 y✝)
 
lctx: ?m.13104
lctx
pure lctx.getFVarIds: TacticM (?m.13111 y✝)
.
getFVarIds: LocalContext β†’ Array FVarId
getFVarIds
    | 
some: {Ξ± : Type ?u.12877} β†’ Ξ± β†’ Option Ξ±
some 
ids: Array Syntax
ids => 
ids: Array Syntax
ids
ids.mapM <| getFVarIdAt goal: TacticM (?m.13111 y✝)
.
mapM: {Ξ± : Type ?u.13307} β†’
  {Ξ² : Type ?u.13306} β†’ {m : Type ?u.13306 β†’ Type ?u.13305} β†’ [inst : Monad m] β†’ (Ξ± β†’ m Ξ²) β†’ Array Ξ± β†’ m (Array Ξ²)
mapM
ids.mapM <| getFVarIdAt goal: TacticM (?m.13111 y✝)
 <| 
getFVarIdAt: MVarId β†’ Syntax β†’ TacticM FVarId
getFVarIdAt
ids.mapM <| getFVarIdAt goal: TacticM (?m.13111 y✝)
 
goal: MVarId
goal
    if 
includeImplementationDetails: optParam Bool false
includeImplementationDetails then
      return 
fvarIds: ?m.13107
fvarIds
    else
      return 
filterOutImplementationDetails: LocalContext β†’ Array FVarId β†’ Array FVarId
filterOutImplementationDetails 
lctx: ?m.13104
lctx 
fvarIds: ?m.13107
fvarIds

/--
Run a tactic on all goals, and always succeeds.

(This is parallel to `Lean.Elab.Tactic.evalAllGoals` in core,
which takes a `Syntax` rather than `TacticM Unit`.
This function could be moved to core and `evalAllGoals` refactored to use it.)
-/
def 
allGoals: TacticM Unit β†’ TacticM Unit
allGoals (
tac: TacticM Unit
tac : 
TacticM: Type β†’ Type
TacticM 
Unit: Type
Unit) : 
TacticM: Type β†’ Type
TacticM 
Unit: Type
Unit := do
  let 
mvarIds: ?m.15695
mvarIds ← 
getGoals: TacticM (List MVarId)
getGoals
  let mut 
mvarIdsNew: ?m.15806
mvarIdsNew := 
#[]: Array ?m.15700
#[]
  for 
mvarId: ?m.15800
mvarId in 
mvarIds: ?m.15695
mvarIds do
    unless 
(← mvarId.isAssigned): ?m.15935
(← 
mvarId: ?m.15800
mvarId
(← mvarId.isAssigned): ?m.15935
.
isAssigned: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadMCtx m] β†’ MVarId β†’ m Bool
isAssigned
(← mvarId.isAssigned): ?m.15935
) do
      
setGoals: List MVarId β†’ TacticM Unit
setGoals [
mvarId: ?m.15800
mvarId]
      try
        
tac: TacticM Unit
tac
        
mvarIdsNew: ?m.15806
mvarIdsNew := 
mvarIdsNew: ?m.15806
mvarIdsNew ++ (← 
getUnsolvedGoals: TacticM (List MVarId)
getUnsolvedGoals)
      catch 
ex: ?m.16735
ex =>
        if 
(← read): ?m.16843
(← 
read: {ρ : outParam (Type ?u.16774)} β†’ {m : Type ?u.16774 β†’ Type ?u.16773} β†’ [self : MonadReader ρ m] β†’ m ρ
read
(← read): ?m.16843
).
recover: Context β†’ Bool
recover then
          
logException: {m : Type β†’ Type} β†’
  [inst : Monad m] β†’
    [inst : MonadLog m] β†’
      [inst : AddMessageContext m] β†’ [inst : MonadOptions m] β†’ [inst : MonadLiftT IO m] β†’ Exception β†’ m Unit
logException 
ex: ?m.16735
ex
          
mvarIdsNew: ?m.15806
mvarIdsNew := 
mvarIdsNew: ?m.15806
mvarIdsNew.
push: {Ξ± : Type ?u.17375} β†’ Array Ξ± β†’ Ξ± β†’ Array Ξ±
push 
mvarId: ?m.15800
mvarId
        else
          
throw: {Ξ΅ : outParam (Type ?u.17552)} β†’
  {m : Type ?u.17551 β†’ Type ?u.17550} β†’ [self : MonadExcept Ξ΅ m] β†’ {Ξ± : Type ?u.17551} β†’ Ξ΅ β†’ m Ξ±
throw 
ex: ?m.16735
ex
  
setGoals: List MVarId β†’ TacticM Unit
setGoals 
mvarIdsNew: ?m.17865
mvarIdsNew.
toList: {Ξ± : Type ?u.17876} β†’ Array Ξ± β†’ List Ξ±
toList

/-- Simulates the `<;>` tactic combinator. First runs `tac1` and then runs
    `tac2` on all newly-generated subgoals.
-/
def 
andThenOnSubgoals: TacticM Unit β†’ TacticM Unit β†’ TacticM Unit
andThenOnSubgoals (
tac1: TacticM Unit
tac1 : 
TacticM: Type β†’ Type
TacticM 
Unit: Type
Unit)  (
tac2: TacticM Unit
tac2 : 
TacticM: Type β†’ Type
TacticM 
Unit: Type
Unit) : 
TacticM: Type β†’ Type
TacticM 
Unit: Type
Unit :=
  
focus: {Ξ± : Type} β†’ TacticM Ξ± β†’ TacticM Ξ±
focus do 
tac1: TacticM Unit
tac1; 
allGoals: TacticM Unit β†’ TacticM Unit
allGoals 
tac2: TacticM Unit
tac2

variable [
Monad: (Type ?u.22993 β†’ Type ?u.22992) β†’ Type (max(?u.22993+1)?u.22992)
Monad 
m: ?m.24569
m] [
MonadExcept: outParam (Type ?u.22285) β†’ (Type ?u.22284 β†’ Type ?u.22283) β†’ Type (max(max?u.22285(?u.22284+1))?u.22283)
MonadExcept 
Exception: Type
Exception 
m: ?m.22256
m]

/-- Repeats a tactic at most `n` times, stopping sooner if the
tactic fails. Always succeeds. -/
def 
iterateAtMost: {m : Type β†’ Type u_1} β†’ [inst : Monad m] β†’ [inst : MonadExcept Exception m] β†’ Nat β†’ m Unit β†’ m Unit
iterateAtMost : 
Nat: Type
Nat β†’ 
m: ?m.22275
m 
Unit: Type
Unit β†’ 
m: ?m.22275
m 
Unit: Type
Unit
| 
0: Nat
0, _ => 
pure: {f : Type ?u.22323 β†’ Type ?u.22322} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.22323} β†’ Ξ± β†’ f Ξ±
pure 
(): Unit
()
| 
n: Nat
n + 1, 
tac: m Unit
tac => try 
tac: m Unit
tac; 
iterateAtMost: Nat β†’ m Unit β†’ m Unit
iterateAtMost 
n: Nat
n 
tac: m Unit
tac catch 
_: ?m.22526
_ => 
pure: {f : Type ?u.22529 β†’ Type ?u.22528} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.22529} β†’ Ξ± β†’ f Ξ±
pure 
(): Unit
()

/-- `iterateExactly' n t` executes `t` `n` times. If any iteration fails, the whole tactic fails.
-/
def 
iterateExactly': Nat β†’ m Unit β†’ m Unit
iterateExactly' : 
Nat: Type
Nat β†’ 
m: ?m.22989
m 
Unit: Type
Unit β†’ 
m: ?m.22989
m 
Unit: Type
Unit
| 
0: Nat
0, _ => 
pure: {f : Type ?u.23037 β†’ Type ?u.23036} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.23037} β†’ Ξ± β†’ f Ξ±
pure 
(): Unit
()
| 
n: Nat
n+1, 
tac: m Unit
tac => 
tac: m Unit
tac *> 
iterateExactly': Nat β†’ m Unit β†’ m Unit
iterateExactly' 
n: Nat
n 
tac: m Unit
tac

/--
`iterateRange m n t`: Repeat the given tactic at least `m` times and
at most `n` times or until `t` fails. Fails if `t` does not run at least `m` times.
-/
def 
iterateRange: Nat β†’ Nat β†’ m Unit β†’ m Unit
iterateRange : 
Nat: Type
Nat β†’ 
Nat: Type
Nat β†’ 
m: ?m.23575
m 
Unit: Type
Unit β†’ 
m: ?m.23575
m 
Unit: Type
Unit
| 
0: Nat
0, 
0: Nat
0, _   => 
pure: {f : Type ?u.23635 β†’ Type ?u.23634} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.23635} β†’ Ξ± β†’ f Ξ±
pure 
(): Unit
()
| 
0: Nat
0, 
b: Nat
b, 
tac: m Unit
tac => 
iterateAtMost: {m : Type β†’ Type ?u.23714} β†’ [inst : Monad m] β†’ [inst : MonadExcept Exception m] β†’ Nat β†’ m Unit β†’ m Unit
iterateAtMost 
b: Nat
b 
tac: m Unit
tac
| (
a: Nat
a+1), 
n: Nat
n, 
tac: m Unit
tac => do 
tac: m Unit
tac; 
iterateRange: Nat β†’ Nat β†’ m Unit β†’ m Unit
iterateRange 
a: Nat
a (
n: Nat
n-
1: ?m.23900
1) 
tac: m Unit
tac

/-- Repeats a tactic until it fails. Always succeeds. -/
partial def 
iterateUntilFailure: {m : Type β†’ Type u_1} β†’ [inst : Monad m] β†’ [inst : MonadExcept Exception m] β†’ m Unit β†’ m Unit
iterateUntilFailure (
tac: m Unit
tac : 
m: ?m.24569
m 
Unit: Type
Unit) : 
m: ?m.24569
m 
Unit: Type
Unit :=
  try 
tac: m Unit
tac; 
iterateUntilFailure: m Unit β†’ m Unit
iterateUntilFailure 
tac: m Unit
tac catch 
_: ?m.24669
_ => 
pure: {f : Type ?u.24672 β†’ Type ?u.24671} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.24672} β†’ Ξ± β†’ f Ξ±
pure 
(): Unit
()

/-- `iterateUntilFailureWithResults` is a helper tactic which accumulates the list of results
obtained from iterating `tac` until it fails. Always succeeds.
-/
partial def 
iterateUntilFailureWithResults: {m : Type β†’ Type u_1} β†’ [inst : Monad m] β†’ [inst : MonadExcept Exception m] β†’ {Ξ± : Type} β†’ m Ξ± β†’ m (List Ξ±)
iterateUntilFailureWithResults {
Ξ±: Type
Ξ± : 
Type: Type 1
Type} (
tac: m Ξ±
tac : 
m: ?m.24876
m 
Ξ±: Type
Ξ±) : 
m: ?m.24876
m (
List: Type ?u.24896 β†’ Type ?u.24896
List 
Ξ±: Type
Ξ±) := do
  try
    let 
a: ?m.24973
a ← 
tac: m Ξ±
tac
    let 
l: ?m.25013
l ← 
iterateUntilFailureWithResults: {Ξ± : Type} β†’ m Ξ± β†’ m (List Ξ±)
iterateUntilFailureWithResults 
tac: m Ξ±
tac
    
pure: {f : Type ?u.25016 β†’ Type ?u.25015} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.25016} β†’ Ξ± β†’ f Ξ±
pure (
a: ?m.24973
a :: 
l: ?m.25013
l)
  catch 
_: ?m.25074
_ => 
pure: {f : Type ?u.25077 β†’ Type ?u.25076} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.25077} β†’ Ξ± β†’ f Ξ±
pure 
[]: List ?m.25102
[]

/-- `iterateUntilFailureCount` is similar to `iterateUntilFailure` except it counts
the number of successful calls to `tac`. Always succeeds.
-/
def 
iterateUntilFailureCount: {Ξ± : Type} β†’ m Ξ± β†’ m Nat
iterateUntilFailureCount {
Ξ±: Type
Ξ± : 
Type: Type 1
Type} (
tac: m Ξ±
tac : 
m: ?m.25287
m 
Ξ±: Type
Ξ±) : 
m: ?m.25287
m 
Nat: Type
Nat := do
  let 
r: ?m.25413
r ← 
iterateUntilFailureWithResults: {m : Type β†’ Type ?u.25365} β†’ [inst : Monad m] β†’ [inst : MonadExcept Exception m] β†’ {Ξ± : Type} β†’ m Ξ± β†’ m (List Ξ±)
iterateUntilFailureWithResults 
tac: m Ξ±
tac
  return 
r: ?m.25413
r.
length: {Ξ± : Type ?u.25440} β†’ List Ξ± β†’ Nat
length

end Lean.Elab.Tactic

namespace Mathlib
open Lean

/-- Returns the root directory which contains the package root file, e.g. `Mathlib.lean`. -/
def 
getPackageDir: String β†’ IO System.FilePath
getPackageDir (
pkg: String
pkg : 
String: Type
String) : 
IO: Type β†’ Type
IO 
System.FilePath: Type
System.FilePath := do
  let 
sp: ?m.25685
sp ← 
initSrcSearchPath: System.FilePath β†’ optParam SearchPath βˆ… β†’ IO SearchPath
initSrcSearchPath 
(← findSysroot): ?m.25644
(← 
findSysroot: optParam String "lean" β†’ IO System.FilePath
findSysroot
(← findSysroot): ?m.25644
)
  let 
root?: ?m.25866
root? ← 
sp: ?m.25685
sp.
findM?: {m : Type β†’ Type ?u.25723} β†’ [inst : Monad m] β†’ {Ξ± : Type} β†’ (Ξ± β†’ m Bool) β†’ List Ξ± β†’ m (Option Ξ±)
findM? fun 
p: ?m.25754
p =>
    (
p: ?m.25754
p / 
pkg: String
pkg).
isDir: System.FilePath β†’ BaseIO Bool
isDir <||> ((
p: ?m.25754
p / 
pkg: String
pkg).
withExtension: System.FilePath β†’ String β†’ System.FilePath
withExtension 
"lean": String
"lean").
pathExists: System.FilePath β†’ BaseIO Bool
pathExists
  if let 
some: {Ξ± : Type ?u.25877} β†’ Ξ± β†’ Option Ξ±
some 
root: System.FilePath
root := 
root?: ?m.25866
root? then return 
root: System.FilePath
root
  
throw: {Ξ΅ : outParam (Type ?u.26400)} β†’
  {m : Type ?u.26399 β†’ Type ?u.26398} β†’ [self : MonadExcept Ξ΅ m] β†’ {Ξ± : Type ?u.26399} β†’ Ξ΅ β†’ m Ξ±
throw <| 
IO.userError: String β†’ IO.Error
IO.userError s!"Could not find {
pkg: String
pkg} directory. {
    
"": String
""}Make sure the LEAN_SRC_PATH environment variable is set correctly."

/-- Returns the mathlib root directory. -/
def 
getMathlibDir: ?m.27571
getMathlibDir := 
getPackageDir: String β†’ IO System.FilePath
getPackageDir 
"Mathlib": String
"Mathlib"