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.

def Char.toUInt8 (n : Char) : UInt8

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

Equations

• Char.toUInt8 n = UInt32.toUInt8 n.val

theorem Char.utf8Size_pos (c : Char) : 0 < Char.utf8Size c

instance instLinearOrderChar : LinearOrder Char

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

Equations

• instLinearOrderChar = LinearOrder.mk instLinearOrderChar.proof_5 inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE

theorem Char.ofNat_toNat {c : Char} (h : Char.isValidCharNat (Char.toNat c)) : Char.ofNat (Char.toNat c) = c