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.

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

Equations

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

Equations
theorem Char.ofNat_toNat {c : Char} (h : ) :
= c