Documentation

Std.Do.SPred.Notation.Basic

source
def Std.Do.«termSpred(_)» :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Std.Do.«termTerm(_)» :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    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

      Remove an spred layer from a term syntax object.