Documentation

Std.Do.SPred.Notation.Basic

source
def Std.Do.«termSpred(_)» :
Lean.ParserDescr

An embedding of the special syntax for SPred into ordinary terms that provides alternative interpretations of logical connectives and quantifiers.

Within spred(...), term(...) escapes to the ordinary Lean interpretation of this syntax.

Instances For
    source
    def Std.Do.«termTerm(_)» :
    Lean.ParserDescr

    Escapes from a surrounding spred(...) term, returning to the usual interpretations of quantifiers and connectives.

    Instances For
      source
      partial def Std.Do.SPred.Notation.unpack {m : Type → Type} [Monad m] [Lean.MonadRef m] [Lean.MonadQuotation m] :
      Lean.Term → m Lean.Term

      Removes an spred layer from a term syntax object.