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

Equations

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

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

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

Remove an spred layer from a term syntax object.

Idiom notation

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

Embedding of pure Lean values into SVal.

Equations

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

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

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

Equations

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

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

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

Equations

• Std.Do.«term#_» = Lean.ParserDescr.node `Std.Do.«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

Sugar for SPred

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

Entailment in SPred; sugar for SPred.entails.

Equations

• Std.Do.«term_⊢ₛ_» = Lean.ParserDescr.trailingNode `Std.Do.«term_⊢ₛ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ₛ ") (Lean.ParserDescr.cat `term 25))

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

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

Equations

• Std.Do.«term⊢ₛ_» = Lean.ParserDescr.node `Std.Do.«term⊢ₛ_» 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ₛ ") (Lean.ParserDescr.cat `term 25))

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

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

Equations

• Std.Do.«term_⊣⊢ₛ_» = Lean.ParserDescr.trailingNode `Std.Do.«term_⊣⊢ₛ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊣⊢ₛ ") (Lean.ParserDescr.cat `term 25))