structure Data.Down (α : Type u) : Type u

Down α reverses the ordering of α.

If $a \leq b$ in α, then $\text{Down}(b) \leq \text{Down}(a)$. Useful for sorting in descending order without custom comparators. $$\text{compare}_{\text{Down}}(x, y) = \text{compare}(y, x)$$

• getDown : α

  Unwrap the reversed-order value.

def Data.instReprDown.repr {α✝ : Type u_1} [Repr α✝] : Down α✝ → Nat → Std.Format

Equations

• Data.instReprDown.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "getDown" ++ Std.Format.text " := " ++ (Std.Format.nest 11 (repr x✝.getDown)).group) " }"

@[implicit_reducible]

instance Data.instReprDown {α✝ : Type u_1} [Repr α✝] : Repr (Down α✝)

Equations

• Data.instReprDown = { reprPrec := Data.instReprDown.repr }

def Data.instHashableDown.hash {α✝ : Type u_1} [Hashable α✝] : Down α✝ → UInt64

Equations

• Data.instHashableDown.hash { getDown := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.instHashableDown {α✝ : Type u_1} [Hashable α✝] : Hashable (Down α✝)

Equations

• Data.instHashableDown = { hash := Data.instHashableDown.hash }

@[implicit_reducible]

instance Data.Down.instBEq {α : Type u_1} [BEq α] : BEq (Down α)

Equations

• Data.Down.instBEq = { beq := fun (a b : Data.Down α) => a.getDown == b.getDown }

@[implicit_reducible]

instance Data.Down.instOrd {α : Type u_1} [Ord α] : Ord (Down α)

Reversed ordering: compares in the opposite direction.

Equations

• Data.Down.instOrd = { compare := fun (a b : Data.Down α) => compare b.getDown a.getDown }

@[implicit_reducible]

instance Data.Down.instToString {α : Type u_1} [ToString α] : ToString (Down α)

Equations

• Data.Down.instToString = { toString := fun (d : Data.Down α) => toString "Down(" ++ toString d.getDown ++ toString ")" }

theorem Data.Down.get_mk {α : Type u_1} (a : α) : { getDown := a }.getDown = a

Wrapping and unwrapping Down is identity. $$\text{getDown}(\text{Down}(x)) = x$$

theorem Data.Down.compare_reverse {α : Type u_1} [Ord α] (a b : Down α) : compare a b = compare b.getDown a.getDown

Down comparison reverses the arguments.

@[inline]

def Data.comparing {β : Type u_1} {α : Sort u_2} [Ord β] (f : α → β) (x y : α) : Ordering

Compare two values by first applying a projection function. $$\text{comparing}(f, x, y) = \text{compare}(f(x), f(y))$$

Useful with sorting: list.mergeSort (comparing SomeStruct.field)

Equations

• Data.comparing f x y = compare (f x) (f y)

def Data.clamp {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x lo hi : α) (hle : lo ≤ hi) (refl : ∀ (a : α), a ≤ a) (total : ∀ (a b : α), ¬a ≤ b → b ≤ a) : { y : α // lo ≤ y ∧ y ≤ hi }

Clamp a value to the interval $[\text{lo}, \text{hi}]$.

Returns a subtype proving the result lies within bounds: $$\text{clamp}(x, lo, hi) = \begin{cases} lo & \text{if } x \leq lo \\ hi & \text{if } x \geq hi \\ x & \text{otherwise} \end{cases}$$

Precondition: lo ≤ hi (provided as proof). Guarantee: The returned value y satisfies lo ≤ y ∧ y ≤ hi.

Equations

• Data.clamp x lo hi hle refl total = if h₁ : x ≤ lo then ⟨lo, ⋯⟩ else if h₂ : hi ≤ x then ⟨hi, ⋯⟩ else ⟨x, ⋯⟩