@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Simproc.andThen (f g : Simproc) : Simproc

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Meta.Sym.Simp.instAndThenSimproc : AndThen Simproc

Equations

• Lean.Meta.Sym.Simp.instAndThenSimproc = { andThen := fun (f : Lean.Meta.Sym.Simp.Simproc) (g : Unit → Lean.Meta.Sym.Simp.Simproc) => f.andThen (g ()) }