Structures · Lean core
Ord
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.
- Defined in
- Init.Data.Ord.Basic
- Shape
- One type argument · adds compare
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Concrete types that are instances100
- Int
- Nat
- Bool
- BitVec
- UInt64
- UInt8
- UInt16
- UInt32
- USize
- Units
- AddUnits
- Int32
- Int8
- Int64
- Int16
- ISize
- Char
- String
- WithTopology
- Vector
- String.Slice
- Std.Time.Month.Offset
- Ordering
- Std.Time.Week.Offset
- Std.Time.Second.Offset
- Std.Time.Minute.Offset
- Std.Time.Nanosecond.Offset
- Std.Time.Day.Offset
- Std.Time.Hour.Offset
- Lean.JsonNumber
- Std.Time.Internal.UnitVal
- Std.Time.Millisecond.Offset
- Std.Time.Year.Offset
- Std.Time.Duration
- Aesop.Percent
- Std.Time.Timestamp
- Std.Time.WallTime
- Aesop.Nanos
- Aesop.RuleName
- Float.Model.UnpackedFloat.Sign
- Lean.Lsp.Position
- Lean.JsonRpc.RequestID
- Aesop.SlotIndex
- IO.TaskState
- Lean.Lsp.Range
- Lean.Meta.DiscrTree.Key
- Lean.Grind.AC.Seq
- Std.Time.PlainDateTime
- Std.Time.PlainDate
- Std.Time.Second.Ordinal
- Std.Time.PlainTime
- Aesop.LevelIndex
- Aesop.PremiseIndex
- Lean.Literal
- Lean.SubExpr.Pos
- Lean.Doc.Inline
- Aesop.PhaseName
- Aesop.DisplayRuleName
- Aesop.BuilderName
- Aesop.ScopeName
- Std.Time.Day.Ordinal.OfYear
- Aesop.ForwardRule
- Std.Time.Week.OfYear.Ordinal
- Std.Time.Nanosecond.Ordinal
- Std.Time.Millisecond.Ordinal
- IO.FS.SystemTime
- Std.Time.Hour.Ordinal
- Std.Time.Day.Ordinal
- Std.Time.Minute.Ordinal
- Std.Time.Month.Ordinal
- Std.Time.Month.Quarter
- Std.Time.Weekday.Ordinal
- Lean.Lsp.RefIdent
- Lean.Doc.Part
- Aesop.ForwardRulePriority
- Lean.Doc.Block
- Lean.Lsp.Location
- Lean.Doc.DescItem
- Aesop.ForwardRuleMatch
- Aesop.Match
- Lean.Lsp.DiagnosticCode
- Std.Time.Week.Ordinal
- Aesop.IndexMatchLocation
- Lean.Lsp.DiagnosticTag
- Lean.Lsp.DiagnosticSeverity
- Lean.Lsp.DiagnosticRelatedInformation
- Lean.Doc.ListItem
- Aesop.Substitution
- Std.Time.Week.Aligned.Ordinal
- Aesop.UnsafeQueueEntry
- Lean.Lsp.LeanDiagnosticTag
- Aesop.CompleteMatch
- Aesop.SafeRuleInfo
- Aesop.Rule
- Aesop.NormRuleInfo
- Std.Time.Nanosecond.Span
- Std.Time.Weekday
- Aesop.UnsafeRuleInfo
- Std.Async.System.UserId
- Std.Async.System.GroupId
How is a type an instance?
Loading the hierarchy index…
Assumed by32
- Equiv.ord
- ULift.instOrd_mathlib
- Function.Injective.linearOrder
- ULift.down_compare
- AddUnits.compare_val
- OrderDual.instOrd
- OrderDual.Ord.dual_dual
- WithTopology.instOrd
- Ord.lex_eq
- Mathlib.Tactic.ClickSuggestions.SectionState.insertResult
- Units.instOrd
- AddUnits.instOrd
- Function.Injective.linearOrderedCommMonoidWithZero
- Units.compare_val
- ULift.instLawfulBEqOrd_mathlib
- ULift.instOrientedOrd_mathlib
- ULift.up_compare
- Prod.Lex.instOrdLexProd
- ULift.instLawfulLTOrd_mathlib
- LinearOrder.liftWithOrd'
- Equiv.ord_def
- Prod.Lex.instOrientedOrdLex
- Mathlib.Tactic.ClickSuggestions.instOrdResult
- Prod.Lex.instTransOrdLex
- lexOrd_eq
- ULift.instLawfulBOrd_mathlib
- ULift.instTransOrd_mathlib
- Mathlib.Tactic.ClickSuggestions.Result.insertInArray
- Mathlib.Tactic.ClickSuggestions.instLTResult
- ULift.instLawfulLEOrd_mathlib
- LinearOrder.liftWithOrd
- Prod.Lex.compare_def
Ancestors0
No ancestors.