← Copula mathematical handbook

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

Equations

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