source
inductive Lean.Elab.Tactic.Grind.Filter :
Type

- true : Filter
- const (declName : Name) : Filter
- fvar (fvarId : FVarId) : Filter
- gen (pred : Nat → Bool) : Filter
- or (a b : Filter) : Filter
- and (a b : Filter) : Filter
- not (a : Filter) : Filter

Instances For

source
def Lean.Elab.Tactic.Grind.elabFilter (filter? : Option (TSyntax `grind_filter)) :
GrindTacticM Filter
Equations

- Lean.Elab.Tactic.Grind.elabFilter (some filter) = Lean.Elab.Tactic.Grind.elabFilter.go✝ filter
- Lean.Elab.Tactic.Grind.elabFilter filter? = pure Lean.Elab.Tactic.Grind.Filter.true

Instances For

source
def Lean.Elab.Tactic.Grind.Filter.eval (filter : Filter) (e : Expr) :
Meta.Grind.GoalM Bool
Equations

- filter.eval e = Lean.Elab.Tactic.Grind.Filter.eval.go✝ e filter

Instances For