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

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

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