Stdlib.Function

Contents

<< {A B C} (f : B -> C) (g : A -> B) (x : A) : CSource #

Function composition, passing results from the second function `g` to the first function `f`.

>> {A B C} (f : A -> B) (g : B -> C) (x : A) : CSource #

Function composition, passing results from the first function `f` to the second function `g`.

const {A B} (a : A) (_ : B) : ASource #

Always returns the first argument `a`.

The identity function.

flip {A B C} (f : A -> B -> C) (b : B) (a : A) : CSource #

Swaps the order of the arguments of the given function `f`.

<| {A B} (f : A -> B) (x : A) : BSource #

Application operator with right associativity. Usually used as a syntactical facility.

|> {A B} (x : A) (f : A -> B) : BSource #

Application operator with left associativity. Usually used as a syntactical facility.

iterate {A} : (n : Nat) -> (fun : A -> A) -> (elem : A) -> ASource #

Applies a function n times.

on {A B C} (f : B -> B -> C) (g : A -> B) (a b : A) : CSource #

`(f on g) a b` is equivalent to `f (g a) (g b)`.

builtin seq >-> : {A B : Type} -> A -> B -> BSource #

Description

Definitions