Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.Epic.LambdaLift
Description
Lift lambda expressions to top level definitions (Epic does not support lambdas).
Synopsis
type LL = WriterT [Fun]
lambdaLift :: MonadTCM m => [Fun] -> Compile m [Fun]
lambdaLiftFun :: MonadTCM m => Fun -> LL (Compile m) Fun
lambdaLiftExpr :: MonadTCM m => Expr -> LL (Compile m) Expr
Documentation
type LL = WriterT [Fun]Source
LL makes it possible to emit new functions when we encounter a lambda
lambdaLift :: MonadTCM m => [Fun] -> Compile m [Fun]Source
lambda lift all the functions
lambdaLiftFun :: MonadTCM m => Fun -> LL (Compile m) FunSource
 lift a function, this is in a LL (Writer monad)
lambdaLiftExpr :: MonadTCM m => Expr -> LL (Compile m) ExprSource
 lift an expression, put all the new definitions in the writer monad
Produced by Haddock version 2.6.1