LowerCase

This module provides predicates and normalization functions for handling ASCII case-insensitivity. It includes proofs of idempotency for lowercase transformations, as well as utilities for validating the lowercase state of a String.

def Std.Http.Internal.IsLowerCase (s : String) : Prop

Predicate asserting that a string is in lowercase form.

Equations

• Std.Http.Internal.IsLowerCase s = (s.toLower = s)

@[implicit_reducible]

instance Std.Http.Internal.instDecidableIsLowerCase {s : String} : Decidable (IsLowerCase s)

Equations

• Std.Http.Internal.instDecidableIsLowerCase = decidable_of_decidable_of_iff ⋯

theorem Std.Http.Internal.IsLowerCase.isLowerCase_toLower {s : String} : IsLowerCase s.toLower

Proof that applying toLower to any string results in a string that satisfies the IsLowerCase predicate.

theorem Std.Http.Internal.IsLowerCase.isLowerCase_empty : IsLowerCase ""