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. An alias for SPred.pure.

Equations

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

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))

def Std.Do.SPred.Notation.unexpandPure : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandEntails : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandBientails : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandAnd : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandOr : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandNot : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandImp : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandForall : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandExists : Lean.PrettyPrinter.Unexpander

Equations

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

def Std.Do.SPred.Notation.unexpandIff : Lean.PrettyPrinter.Unexpander

Equations

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