@[inline]

def Data.Function.on {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} (f : β → β → γ) (g : α → β) (x y : α) : γ

The on combinator lifts a binary function through a unary projection:

$$(\texttt{on}\; f\; g)\; x\; y \;=\; f\,(g\,x)\,(g\,y)$$

Commonly used to compare or combine values by a derived key, e.g., on compare String.length compares strings by length.

Equations

• Data.Function.on f g x y = f (g x) (g y)

@[inline]

def Data.Function.applyTo {α : Sort u_1} {β : Sort u_2} (x : α) (f : α → β) : β

Flip of function application (Haskell's (&) operator):

$$\texttt{applyTo}\; x\; f \;=\; f\,x$$

Useful for piping a value through a chain of transformations.

Equations

• Data.Function.applyTo x f = f x

@[inline]

def Data.Function.const {α : Sort u_1} {β : Sort u_2} (a : α) : β → α

The constant combinator $K$:

$$\texttt{const}\; a\; b \;=\; a$$

Ignores its second argument and always returns the first. In combinatory logic this is the $K$ combinator.

Equations

• Data.Function.const a x✝ = a

@[inline]

def Data.Function.flip {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) (b : β) (a : α) : γ

Flip the argument order of a binary function:

$$\texttt{flip}\; f\; b\; a \;=\; f\; a\; b$$

In combinatory logic this is the $C$ combinator.

Equations

• Data.Function.flip f b a = f a b

theorem Data.Function.on_apply {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} (f : β → β → γ) (g : α → β) (x y : α) : on f g x y = f (g x) (g y)

on unfolds to its definition: $(\texttt{on}\; f\; g)\; x\; y = f\,(g\,x)\,(g\,y)$.

theorem Data.Function.applyTo_apply {α : Sort u_1} {β : Sort u_2} (x : α) (f : α → β) : applyTo x f = f x

applyTo unfolds to function application: $\texttt{applyTo}\; x\; f = f\,x$.

theorem Data.Function.const_apply {α : Sort u_1} {β : Sort u_2} (a : α) (b : β) : const a b = a

const ignores its second argument: $\texttt{const}\; a\; b = a$.

theorem Data.Function.flip_flip {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) : flip (flip f) = f

flip is an involution — flipping twice recovers the original function:

$$\texttt{flip}\,(\texttt{flip}\; f) = f$$

theorem Data.Function.flip_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) (a : α) (b : β) : flip f b a = f a b

flip swaps the arguments: $\texttt{flip}\; f\; b\; a = f\; a\; b$.