Documentation

Mathlib.Data.Char

More Char instances #

This file provides a LinearOrder instance on Char. Char is the type of Unicode scalar values. Provides an additional definition to truncate a Char to UInt8 and a theorem on conversion to Nat.

source
def Char.toUInt8 (n : Char) :
UInt8

Convert a character into a UInt8, by truncating (reducing modulo 256) if necessary.

Equations
Instances For
    source
    theorem Char.utf8Size_pos (c : Char) :
    0 < Char.utf8Size c
    source
    instance instLinearOrderChar :
    LinearOrder Char

    Provides a LinearOrder instance on Char. Char is the type of Unicode scalar values.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem Char.ofNat_toNat {c : Char} (h : Char.isValidCharNat (Char.toNat c)) :
    Char.ofNat (Char.toNat c) = c