mathlib3 documentation

data.char

More char instances #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides a linear_order instance on char. char is the type of Unicode scalar values.

@[protected, instance]
Equations