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.

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

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

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.