2cf3ac9461
This PR splits `Std.Classes.Ord` into `Std.Classes.Ord.Basic` (with few imports) and `Std.Classes.Ord.SInt` and `Std.Classes.Ord.Vector`. These changes avoid importing `Init.Data.BitVec.Lemmas` unnecessarily into various basic files. As the new import-only file `Std.Classes.Ord` imports all three of these, end-users are not affected.
40 lines
978 B
Text
40 lines
978 B
Text
/-
|
|
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Markus Himmel, Paul Reichert, Robin Arnez
|
|
-/
|
|
prelude
|
|
import Std.Classes.Ord.Basic
|
|
import Init.Data.String.Lemmas
|
|
|
|
/-!
|
|
# Instances for strings.
|
|
|
|
-/
|
|
|
|
set_option autoImplicit false
|
|
set_option linter.missingDocs true
|
|
|
|
open Std
|
|
|
|
namespace String
|
|
|
|
instance : TransOrd String :=
|
|
TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
|
|
String.le_antisymm String.le_trans String.le_total String.not_le
|
|
|
|
instance : LawfulEqOrd String where
|
|
eq_of_compare h := compareOfLessAndEq_eq_eq String.le_refl String.not_le |>.mp h
|
|
|
|
end String
|
|
|
|
namespace Char
|
|
|
|
instance : TransOrd Char :=
|
|
TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
|
|
Char.le_antisymm Char.le_trans Char.le_total Char.not_le
|
|
|
|
instance : LawfulEqOrd Char where
|
|
eq_of_compare h := compareOfLessAndEq_eq_eq Char.le_refl Char.not_le |>.mp h
|
|
|
|
end Char
|