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

Unexpander that reconstructs ⌜...⌝ syntax from applications of SPred.pure.

Equations

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

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

Unexpander that reconstructs ... ⊢ₛ ...⌝ syntax from applications of SPred.entails.

Equations

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

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

Unexpander that reconstructs ... ⊣⊢ₛ ...⌝ syntax from applications of SPred.entails.

Equations

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

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

Unexpander that reconstructs spred(... ∧ ...)⌝ syntax from applications of SPred.and, lifting nested applications of spred(...) from the arguments.

Equations

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

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

Unexpander that reconstructs spred(... ∨ ...)⌝ syntax from applications of SPred.or, lifting nested applications of spred(...) from the arguments.

Equations

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

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

Unexpander that reconstructs spred(¬ ...)⌝ syntax from applications of SPred.not, lifting nested applications of spred(...) from the argument.

Equations

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

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

Unexpander that reconstructs spred(... → ...)⌝ syntax from applications of SPred.imp, lifting nested applications of spred(...) from the arguments.

Equations

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

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

Unexpander that reconstructs spred(∀ ..., ...)⌝ syntax from applications of SPred.forall, lifting nested applications of spred(...) from the body.

Equations

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

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

Unexpander that reconstructs spred(∃ ..., ...)⌝ syntax from applications of SPred.exists, lifting nested applications of spred(...) from the body.

Equations

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

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

Unexpander that reconstructs spred(... ↔ ...)⌝ syntax from applications of SPred.iff, lifting nested applications of spred(...) from the arguments.

Equations

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