Stdlib.Function

Contents

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

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

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

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

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

Always returns the first argument.

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.

<| {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} : Nat -> (A -> A) -> A -> ASource #

Applies a function n times.

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

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

Description

Definitions