Idris2Doc : Data.Fun.Extra

Data.Fun.Extra

Pointwise : (a -> b -> Type) -> Vectna -> Vectnb -> Type
Totality: total
Constructors:
Nil : PointwiserNilNil
(::) : rts -> Pointwisertsss -> Pointwiser (t::ts) (s::ss)
applyPartially : Fun (ts++ss) cod -> HVectts -> Funsscod
Apply an n-ary function to an n-ary tuple of inputs
Totality: total
chainUncurry : (g : Funtsr) -> (f : (r -> r')) -> (elems : HVectts) -> f (uncurrygelems) = uncurry (chainfg) elems
Uncurrying a Fun and then composing with a normal function
is extensionally equal to
composing functions using `chain`, then uncurrying.
Totality: total
curry : (HVectts -> cod) -> Funtscod
Apply an n-ary function to an n-ary tuple of inputs
Totality: total
curryAll : ((xs : HVectts) -> uncurrycodxs) -> Alltscod
Totality: total
extractWitness : Extsr -> HVectts
Totality: total
extractWitnessCorrect : (f : Extsr) -> uncurryr (extractWitnessf)
Totality: total
homoAllNeut_ext : FunNilcod -> idcod
Totality: total
homoFunMult_ext : Fun (rs++ss) cod -> . (Funrs) (Funss) cod
Totality: total
homoFunMult_inv : . (Funrs) (Funss) cod -> Fun (rs++ss) cod
Totality: total
homoFunNeut_ext : FunNilcod -> idcod
Totality: total
homoFunNeut_inv : idcod -> FunNilcod
Totality: total
introduceWitness : (witness : HVectts) -> uncurryrwitness -> Extsr
Totality: total
precompose : Pointwise (\a, b => a -> b) tsss -> Funsscod -> Funtscod
Totality: total
uncurry : Funtscod -> HVectts -> cod
Apply an n-ary function to an n-ary tuple of inputs
Totality: total
uncurryAll : Alltscod -> (xs : HVectts) -> uncurrycodxs
Apply an n-ary dependent function to its tuple of inputs (given by an HVect)
Totality: total