Documentation

Lean.Meta.Tactic.Grind.Combinators

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

def Lean.Meta.Grind.GrindTactic :

Equations

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

Instances For

def Lean.Meta.Grind.GrindTactic.try (x : 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) :

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) :

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) :

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) :

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' :

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') :

Equations

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