← Copula mathematical handbook

inductive Lean.Meta.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.Meta.Grind.Filter.eval (filter : Filter) (e : Expr) : GoalM Bool

Equations

• filter.eval e = Lean.Meta.Grind.Filter.eval.go✝ e filter