Idris2Doc : Data.Fun.Extra

Data.Fun.Extra

data Pointwise : (a -> b -> Type) -> Vect n a -> Vect n b -> Type
  Totality: total
  Constructors:
  
Nil : Pointwise r [] []
  
(::) : r t s -> Pointwise r ts ss -> Pointwise r (t :: ts) (s :: ss)
applyPartially : Fun (ts ++ ss) cod -> HVect ts -> Fun ss cod
  Apply an n-ary function to an n-ary tuple of inputs

  Totality: total
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
curry : (HVect ts -> cod) -> Fun ts cod
  Apply an n-ary function to an n-ary tuple of inputs

  Totality: total
curryAll : ((xs : HVect ts) -> uncurry cod xs) -> All ts cod
  Totality: total
extractWitness : Ex ts r -> HVect ts
  Totality: total
extractWitnessCorrect : (f : Ex ts r) -> uncurry r (extractWitness f)
  Totality: total
homoAllNeut_ext : Fun [] cod -> id cod
  Totality: total
homoFunMult_ext : Fun (rs ++ ss) cod -> . (Fun rs) (Fun ss) cod
  Totality: total
homoFunMult_inv : . (Fun rs) (Fun ss) cod -> Fun (rs ++ ss) cod
  Totality: total
homoFunNeut_ext : Fun [] cod -> id cod
  Totality: total
homoFunNeut_inv : id cod -> Fun [] cod
  Totality: total
introduceWitness : (witness : HVect ts) -> uncurry r witness -> Ex ts r
  Totality: total
precompose : Pointwise (\a, b => a -> b) ts ss -> Fun ss cod -> Fun ts cod
  Totality: total
uncurry : Fun ts cod -> HVect ts -> cod
  Apply an n-ary function to an n-ary tuple of inputs

  Totality: total
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