@[reducible, inline]

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

@[implicit_reducible]

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

@[reducible, inline]

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

@[implicit_reducible]

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

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