Safe Haskell | None |
---|---|
Language | Haskell2010 |
Meta-functions relating to functions.
Documentation
constPartial :: TermLike term TyName Name uni fun => term () -> term () Source #
const
as a PLC term.
constPartial t = /\(A :: *) -> \(x : A) -> t
etaExpand :: TermLike term TyName Name uni fun => Type TyName uni () -> term () -> term () Source #
Eta-expand a function at a given type. Note that this has to be a "meta" function for it not force the function it receives and instead directly hide it under a lambda.
etaExpand ty fun = \(x : ty) -> fun x