Data.Fun.Extra

Definitions

uncurry : Fun ts cod -> HVect ts -> cod

  Apply an n-ary function to an n-ary tuple of inputs

Totality: total
Visibility: public export

curry : (HVect ts -> cod) -> Fun ts cod

  Apply an n-ary function to an n-ary tuple of inputs

Totality: total
Visibility: public export

homoFunNeut_ext : Fun [] cod -> id cod

Totality: total
Visibility: public export

homoFunMult_ext : Fun (rs ++ ss) cod -> (.) (Fun rs) (Fun ss) cod

Totality: total
Visibility: public export

homoFunNeut_inv : id cod -> Fun [] cod

Totality: total
Visibility: public export

homoFunMult_inv : (.) (Fun rs) (Fun ss) cod -> Fun (rs ++ ss) cod

Totality: total
Visibility: public export

applyPartially : Fun (ts ++ ss) cod -> HVect ts -> Fun ss cod

  Apply an n-ary function to an n-ary tuple of inputs

Totality: total
Visibility: public export

uncurryAll : All ts cod -> (xs : HVect ts) -> uncurry cod xs

  Apply an n-ary dependent function to its tuple of inputs (given by an HVect)

Totality: total
Visibility: public export

curryAll : ((xs : HVect ts) -> uncurry cod xs) -> All ts cod

Totality: total
Visibility: public export

homoAllNeut_ext : Fun [] cod -> id cod

Totality: total
Visibility: public export

extractWitness : Ex ts r -> HVect ts

Totality: total
Visibility: public export

extractWitnessCorrect : (f : Ex ts r) -> uncurry r (extractWitness f)

Totality: total
Visibility: public export

introduceWitness : (witness : HVect ts) -> uncurry r witness -> Ex ts r

Totality: total
Visibility: public export

data Pointwise : (a -> b -> Type) -> Vect n a -> Vect n b -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Pointwise r [] []

(::) : r t s -> Pointwise r ts ss -> Pointwise r (t :: ts) (s :: ss)

precompose : Pointwise (\a, b => a -> b) ts ss -> Fun ss cod -> Fun ts cod

Totality: total
Visibility: public export

chainUncurry : (g : Fun ts r) -> (f : (r -> r')) -> (elems : HVect ts) -> f (uncurry g elems) = uncurry (chain f g) elems

  Uncurrying a Fun and then composing with a normal function
  is extensionally equal to
  composing functions using `chain`, then uncurrying.

Totality: total
Visibility: public export