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

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

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.

Idiom notation

def Std.Do.«term⌜_⌝» : Lean.ParserDescr

Embedding of pure Lean values into SVal.

def Std.Do.«term‹_›ₛ» : Lean.ParserDescr

‹t› in SVal idiom notation. Accesses the state of type t.

def Std.Do.«term#_» : Lean.ParserDescr

Use getter t : SVal σs σ in SVal idiom notation; sugar for SVal.uncurry t (by assumption).

Sugar for SPred

def Std.Do.«term_⊢ₛ_» : Lean.TrailingParserDescr

Entailment in SPred; sugar for SPred.entails.

def Std.Do.«term⊢ₛ_» : Lean.ParserDescr

Tautology in SPred; sugar for SPred.entails ⌜True⌝.

def Std.Do.«term_⊣⊢ₛ_» : Lean.TrailingParserDescr

Bi-entailment in SPred; sugar for SPred.bientails.