module Stdlib.Function;

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

syntax operator ∘ composition;

--- Function composition.
{-# inline: 2 #-}
∘ {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x);

--- Always returns the first argument.
{-# inline: 1 #-}
const {A B} (a : A) (_ : B) : A := a;

--- The identity function.
id {A} (a : A) : A := a;

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

syntax operator $ rapp;

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

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

syntax operator on lapp;

{-# inline: 2 #-}
on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C := f (g a) (g b);

syntax operator >>> seq;

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