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
- char.linear_order = {le := has_le.le char.has_le, lt := has_lt.lt char.has_lt, le_refl := char.linear_order._proof_1, le_trans := char.linear_order._proof_2, lt_iff_le_not_le := char.linear_order._proof_3, le_antisymm := char.linear_order._proof_4, le_total := char.linear_order._proof_5, decidable_le := char.decidable_le, decidable_eq := char.decidable_eq, decidable_lt := char.decidable_lt, max := max_default (λ (a b : char), a.decidable_le b), max_def := char.linear_order._proof_10, min := min_default (λ (a b : char), a.decidable_le b), min_def := char.linear_order._proof_11}