-
Notifications
You must be signed in to change notification settings - Fork 251
/
Char.lean
34 lines (29 loc) · 1.18 KB
/
Char.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Mathlib.Init.Data.Nat.Lemmas
import Mathlib.Init.Order.Defs
import Mathlib.Data.Nat.Defs
#align_import data.char from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
/-!
# 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`.
-/
/--
Provides a `LinearOrder` instance on `Char`. `Char` is the type of Unicode scalar values.
-/
instance : LinearOrder Char where
le_refl := fun _ => @le_refl ℕ _ _
le_trans := fun _ _ _ => @le_trans ℕ _ _ _ _
le_antisymm := fun _ _ h₁ h₂ => Char.eq_of_val_eq <| UInt32.eq_of_val_eq <| Fin.ext <|
@le_antisymm ℕ _ _ _ h₁ h₂
lt_iff_le_not_le := fun _ _ => @lt_iff_le_not_le ℕ _ _ _
le_total := fun _ _ => @le_total ℕ _ _ _
min := fun a b => if a ≤ b then a else b
max := fun a b => if a ≤ b then b else a
decidableLE := inferInstance
#align char.of_nat_to_nat Char.ofNat_toNat