Documentation

Lean.Meta.Sym.Simp.Simproc

source
@[reducible, inline]
abbrev Lean.Meta.Sym.Simp.Simproc.andThen (f g : Simproc) :
Simproc
Instances For
    source
    @[implicit_reducible]
    instance Lean.Meta.Sym.Simp.instAndThenSimproc :
    AndThen Simproc
    source
    @[reducible, inline]
    abbrev Lean.Meta.Sym.Simp.Simproc.orElse (f g : Simproc) :
    Simproc
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Meta.Sym.Simp.instOrElseSimproc :
      OrElse Simproc
      source
      @[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).

      Instances For