Documentation

Std.Http.Internal.LowerCase

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.

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

Predicate asserting that a string is in lowercase form.

Instances For
    source
    @[implicit_reducible]
    instance Std.Http.Internal.instDecidableIsLowerCase {s : String} :
    Decidable (IsLowerCase s)
    source
    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.

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