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
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.