module Stdlib.Function;

open import Stdlib.Data.Nat.Base;
open import Stdlib.Data.Product.Base;

infixr 9 ∘;
--- Function composition.
∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C;
∘ f g x := f (g x);

--- Always returns the first argument.
const : {A : Type} → {B : Type} → A → B → A;
const a _ := a;

--- The identity function.
id : {A : Type} → A → A;
id a := a;

--- Swaps the order of the arguments of the given function.
flip : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → B → A → C;
flip f b a := f a b;

infixr 0 $;
--- Application operator with right associativity. Usually used as a syntactical
--- facility.
$ : {A : Type} → {B : Type} → (A → B) → A → B;
$ f x := f x;

--- Applies a function n times.
iterate : {A : Type} -> Nat -> (A -> A) -> A -> A;
iterate zero _ a := a;
iterate (suc n) f a := iterate n f (f a);

infixl 0 on;
on : {A : Type} → {B : Type} → {C : Type} → (B → B → C) → (A → B) → A → A → C;
on f g a b := f (g a) (g b);

infixl 1 >>>;
builtin seq
>>> : {A B : Type} → A → B → B;
>>> x y := y;