Combinators for manipulating GrindTactics. TODO: a proper tactic language for grind.

def Lean.Meta.Grind.GrindTactic : Type

Equations

• Lean.Meta.Grind.GrindTactic = (Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM (Option (List Lean.Meta.Grind.Goal)))

def Lean.Meta.Grind.GrindTactic.try (x : GrindTactic) : GrindTactic

Equations

• x.try g = do let __discr ← x g match __discr with | some gs => pure (some gs) | x => pure (some [g])

def Lean.Meta.Grind.applyToAll (x : GrindTactic) (goals : List Goal) : GrindM (List Goal)

Equations

• Lean.Meta.Grind.applyToAll x goals = Lean.Meta.Grind.applyToAll.go x goals []

def Lean.Meta.Grind.applyToAll.go (x : GrindTactic) (goals acc : List Goal) : GrindM (List Goal)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.applyToAll.go x [] acc = pure acc.reverse

def Lean.Meta.Grind.GrindTactic.andThen (x y : GrindTactic) : GrindTactic

Equations

• x.andThen y goal = do let __discr ← x goal match __discr with | some goals => do let a ← Lean.Meta.Grind.applyToAll y goals pure (some a) | x => pure none

instance Lean.Meta.Grind.instAndThenGrindTactic : AndThen GrindTactic

Equations

• Lean.Meta.Grind.instAndThenGrindTactic = { andThen := fun (a : Lean.Meta.Grind.GrindTactic) (b : Unit → Lean.Meta.Grind.GrindTactic) => a.andThen (b ()) }

def Lean.Meta.Grind.GrindTactic.iterate (x : GrindTactic) : GrindTactic

Equations

• x.iterate goal = do let a ← Lean.Meta.Grind.GrindTactic.iterate.go x [goal] [] pure (some a)

partial def Lean.Meta.Grind.GrindTactic.iterate.go (x : GrindTactic) (todo result : List Goal) : GrindM (List Goal)

def Lean.Meta.Grind.GrindTactic.orElse (x y : GrindTactic) : GrindTactic

Equations

• x.orElse y goal = do let __discr ← x goal match __discr with | some goals => pure (some goals) | x => y goal

instance Lean.Meta.Grind.instOrElseGrindTactic : OrElse GrindTactic

Equations

• Lean.Meta.Grind.instOrElseGrindTactic = { orElse := fun (a : Lean.Meta.Grind.GrindTactic) (b : Unit → Lean.Meta.Grind.GrindTactic) => a.andThen (b ()) }

def Lean.Meta.Grind.toGrindTactic (f : GoalM Unit) : GrindTactic

Equations

• Lean.Meta.Grind.toGrindTactic f goal = do let goal ← Lean.Meta.Grind.GoalM.run' goal f if goal.inconsistent = true then pure (some []) else pure (some [goal])

def Lean.Meta.Grind.GrindTactic' : Type

Equations

• Lean.Meta.Grind.GrindTactic' = (Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal))

def Lean.Meta.Grind.GrindTactic'.toGrindTactic (x : GrindTactic') : GrindTactic

Equations

• x.toGrindTactic goal = do let goals ← x goal pure (some goals)