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.

Instances For

    Sugar for SPred #

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

    Entailment in SPred; sugar for SPred.entails.

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

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

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

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

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

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

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

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

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

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

              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.

                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.

                  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.

                    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.

                      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.

                        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.

                          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.

                            Instances For