Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Ord

Lean: Hale.Base.Ord | Haskell: Data.Ord

Overview

Ordering utilities. Down reverses the comparison order. comparing lifts comparisons through projections. clamp returns a proof-carrying bounded value.

API Mapping

LeanHaskellKind
DownDownType
comparingcomparingFunction
clampclampFunction (returns {y // lo <= y /\ y <= hi})

Instances

  • BEq (Down a) (requires BEq a)
  • Ord (Down a) (requires Ord a, reversed)
  • ToString (Down a) (requires ToString a)

Proofs & Guarantees

  • get_mk — (Down.mk x).get = x
  • compare_reverse — compare (Down.mk a) (Down.mk b) = compare b a

Example

-- Down reverses comparison order
compare (Down.mk 3) (Down.mk 7)
-- => Ordering.gt  (because 3 < 7, but Down reverses it)