From 8736e730671c69cebd4a1e0404b28be1a8b6799f Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 10 Apr 2024 22:08:43 +1000 Subject: [PATCH] doc: doc-string for Ord and Ord.compare --- 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 1ae46bd51d2f..47eb9e719874 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)