From cd02ad76f1c10d886d1d90ffde37a3e68765bd46 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 12 Apr 2024 02:02:33 +1000 Subject: [PATCH] doc: doc-string for Ord and Ord.compare (#3861) Hopefully one day we will be able to do a thorough refactor of the computable order types in Lean... In the meantime, some doc-strings. --- src/Init/Data/Ord.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean index 1ae46bd51d..47eb9e7198 100644 --- a/src/Init/Data/Ord.lean +++ b/src/Init/Data/Ord.lean @@ -114,7 +114,18 @@ by `cmp₂` to break the tie. @[inline] def compareLex (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering := (cmp₁ a b).then (cmp₂ a b) +/-- +`Ord α` provides a computable total order on `α`, in terms of the +`compare : α → α → Ordering` function. + +Typically instances will be transitive, reflexive, and antisymmetric, +but this is not enforced by the typeclass. + +There is a derive handler, so appending `deriving Ord` to an inductive type or structure +will attempt to create an `Ord` instance. +-/ class Ord (α : Type u) where + /-- Compare two elements in `α` using the comparator contained in an `[Ord α]` instance. -/ compare : α → α → Ordering export Ord (compare)