Documentation

Std.Do.SPred.Notation

Idiom notation #

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

Embedding of pure Lean values into SVal. An alias for SPred.pure.

Equations
    Instances For

      Sugar for SPred #

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

      Entailment in SPred; sugar for SPred.entails.

      Equations
        Instances For
          source
          def Std.Do.«term⊢ₛ_» :
          Lean.ParserDescr

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

          Equations
            Instances For
              source
              def Std.Do.«term_⊣⊢ₛ_» :
              Lean.TrailingParserDescr

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

              Equations
                Instances For
                  source
                  def Std.Do.SPred.Notation.unexpandPure :
                  Lean.PrettyPrinter.Unexpander

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

                  Equations
                    Instances For
                      source
                      def Std.Do.SPred.Notation.unexpandEntails :
                      Lean.PrettyPrinter.Unexpander

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

                      Equations
                        Instances For
                          source
                          def Std.Do.SPred.Notation.unexpandBientails :
                          Lean.PrettyPrinter.Unexpander

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

                          Equations
                            Instances For
                              source
                              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
                                Instances For
                                  source
                                  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
                                    Instances For
                                      source
                                      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
                                        Instances For
                                          source
                                          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
                                            Instances For
                                              source
                                              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
                                                Instances For
                                                  source
                                                  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
                                                    Instances For
                                                      source
                                                      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
                                                        Instances For