@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.DSimproc.andThen (f g : DSimproc) : DSimproc

Equations

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

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instAndThenDSimproc : AndThen DSimproc

Equations

• Lean.Meta.Sym.DSimp.instAndThenDSimproc = { andThen := fun (f : Lean.Meta.Sym.DSimp.DSimproc) (g : Unit → Lean.Meta.Sym.DSimp.DSimproc) => f.andThen (g ()) }

@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.DSimproc.orElse (f g : DSimproc) : DSimproc

Equations

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

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instOrElseDSimproc : OrElse DSimproc

Equations

• Lean.Meta.Sym.DSimp.instOrElseDSimproc = { orElse := fun (f : Lean.Meta.Sym.DSimp.DSimproc) (g : Unit → Lean.Meta.Sym.DSimp.DSimproc) => f.orElse (g ()) }

@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.DSimproc.tryCatch (f : DSimproc) : DSimproc

Wraps a DSimproc 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.