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.

Equations

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

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

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

Equations

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

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.