@[reducible, inline]

abbrev Web.Cookie.CookiePair : Type

A parsed cookie key-value pair.

Equations

• Web.Cookie.CookiePair = (String × String)

def Web.Cookie.parseCookies (header : String) : List CookiePair

Parse a Cookie header value into key-value pairs. Cookie header format: "name1=value1; name2=value2" $$\text{parseCookies} : \text{String} \to \text{List CookiePair}$$

Equations

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

def Web.Cookie.renderCookies (cookies : List CookiePair) : String

Render a list of cookie pairs into a Cookie header value. $$\text{renderCookies} : \text{List CookiePair} \to \text{String}$$

Equations

• Web.Cookie.renderCookies cookies = "; ".intercalate (List.map (fun (x : Web.Cookie.CookiePair) => match x with | (k, v) => k ++ "=" ++ v) cookies)

inductive Web.Cookie.SameSite : Type

SameSite attribute for Set-Cookie.

• strict : SameSite
• lax : SameSite
• none_ : SameSite

@[implicit_reducible]

instance Web.Cookie.instBEqSameSite : BEq SameSite

Equations

• Web.Cookie.instBEqSameSite = { beq := Web.Cookie.instBEqSameSite.beq }

def Web.Cookie.instBEqSameSite.beq : SameSite → SameSite → Bool

Equations

• Web.Cookie.instBEqSameSite.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Web.Cookie.instReprSameSite.repr : SameSite → Nat → Std.Format

Equations

• Web.Cookie.instReprSameSite.repr Web.Cookie.SameSite.strict prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Web.Cookie.SameSite.strict")).group prec✝
• Web.Cookie.instReprSameSite.repr Web.Cookie.SameSite.lax prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Web.Cookie.SameSite.lax")).group prec✝
• Web.Cookie.instReprSameSite.repr Web.Cookie.SameSite.none_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Web.Cookie.SameSite.none_")).group prec✝

@[implicit_reducible]

instance Web.Cookie.instReprSameSite : Repr SameSite

Equations

• Web.Cookie.instReprSameSite = { reprPrec := Web.Cookie.instReprSameSite.repr }

structure Web.Cookie.SetCookie : Type

Set-Cookie configuration.

• name : String
• value : String
• path : Option String
• domain : Option String
• maxAge : Option Nat
• secure : Bool
• httpOnly : Bool
• sameSite : Option SameSite

def Web.Cookie.renderSetCookie (sc : SetCookie) : String

Render a SetCookie as a Set-Cookie header value. $$\text{renderSetCookie} : \text{SetCookie} \to \text{String}$$

Equations

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

def Web.Cookie.parseSetCookie (header : String) : Option SetCookie

Parse a Set-Cookie header value into a SetCookie structure. Only parses the name=value part; attributes are parsed best-effort. $$\text{parseSetCookie} : \text{String} \to \text{Option SetCookie}$$

Equations

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