@[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.

@[implicit_reducible]

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 ()) }

@[reducible, inline]

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

Equations

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

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instOrElseSimproc : OrElse Simproc

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Simproc.tryCatch (f : Simproc) : Simproc

Wraps a simproc so that any exception is caught and treated as .rfl (no rewrite).

Equations

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