Documentation

Std.Internal.Http.Data.Version

Version #

This module defines Version, the set of HTTP protocol versions modeled by this library.

Reference: https://httpwg.org/specs/rfc9110.html#protocol.version

source
inductive Std.Http.Version :
Type

HTTP protocol versions modeled by this library.

Reference: https://httpwg.org/specs/rfc9110.html#protocol.version

Instances For
    source
    def Std.Http.instReprVersion.repr :
    Version → Nat → Format
    Instances For
      source
      @[implicit_reducible]
      instance Std.Http.instReprVersion :
      Repr Version
      source
      def Std.Http.instInhabitedVersion.default :
      Version
      Instances For
        source
        @[implicit_reducible]
        instance Std.Http.instInhabitedVersion :
        Inhabited Version
        source
        def Std.Http.instBEqVersion.beq :
        Version → Version → Bool
        Instances For
          source
          @[implicit_reducible]
          instance Std.Http.instBEqVersion :
          BEq Version
          source
          @[implicit_reducible]
          instance Std.Http.instDecidableEqVersion :
          DecidableEq Version
          source
          def Std.Http.Version.ofNumber? :
          Nat → Nat → Option Version

          Converts a pair of Nat to the corresponding Version.

          Instances For
            source
            def Std.Http.Version.ofString? :
            String → Option Version

            Converts String to the corresponding Version.

            Instances For
              source
              def Std.Http.Version.ofString! (s : String) :
              Version

              Converts String to the corresponding Version, panics if invalid.

              Instances For
                source
                def Std.Http.Version.toNumber :
                Version → Nat × Nat

                Converts a Version to its corresponding major and minor numbers as a pair.

                Instances For
                  source
                  @[implicit_reducible]
                  instance Std.Http.Version.instToString :
                  ToString Version