Safe Haskell | Safe-Inferred |
---|---|
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