Documentation

Std.Internal.Http.Data.Headers.Value

Header Values #

This module defines the Value type, which represents validated HTTP header values that conform to HTTP standards.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-values

source
@[reducible, inline]
abbrev Std.Http.Header.IsValidHeaderValue (s : String) :
Prop

Proposition that asserts all characters in a string are valid for HTTP header values, and that the first and last characters (if present) are field-vchar (not SP/HTAB).

field-value = field-content field-content = field-vchar [ 1( SP / HTAB / field-vchar ) field-vchar ]

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5.5

Instances For
    source
    structure Std.Http.Header.Value :
    Type

    A validated HTTP header value that ensures all characters conform to HTTP standards.

    Instances For
      source
      def Std.Http.Header.instBEqValue.beq :
      Value → Value → Bool
      Instances For
        source
        @[implicit_reducible]
        instance Std.Http.Header.instBEqValue :
        BEq Value
        source
        def Std.Http.Header.instDecidableEqValue.decEq (x✝ x✝¹ : Value) :
        Decidable (x✝ = x✝¹)
        Instances For
          source
          @[implicit_reducible]
          instance Std.Http.Header.instDecidableEqValue :
          DecidableEq Value
          source
          def Std.Http.Header.instReprValue.repr :
          Value → Nat → Format
          Instances For
            source
            @[implicit_reducible]
            instance Std.Http.Header.instReprValue :
            Repr Value
            source
            @[implicit_reducible]
            instance Std.Http.Header.instHashableValue :
            Hashable Value
            source
            @[implicit_reducible]
            instance Std.Http.Header.instInhabitedValue :
            Inhabited Value
            source
            def Std.Http.Header.Value.ofString? (s : String) :
            Option Value

            Attempts to create a Value from a String, returning none if the string contains invalid characters for HTTP header values.

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

              Creates a Value from a string, panicking with an error message if the string contains invalid characters for HTTP header values.

              Instances For
                source
                def Std.Http.Header.Value.is (s : Value) (h : String) :
                Bool

                Performs a case-insensitive comparison between a Value and a String. Returns true if they match.

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