Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.Epic.ConstructorIrrelevancy
Description
Remove forced (irrelevant) arguments from constructors.
Synopsis
irrFilter :: Type -> IrrFilter
constrIrr :: MonadTCM m => [Fun] -> Compile m [Fun]
irrFun :: MonadTCM m => Fun -> Compile m Fun
irrExpr :: MonadTCM m => Expr -> Compile m Expr
irrBranch :: MonadTCM m => Branch -> Compile m Branch
Documentation
irrFilter :: Type -> IrrFilterSource
Check which arguments are forced and create an IrrFilter
constrIrr :: MonadTCM m => [Fun] -> Compile m [Fun]Source
Remove irrelevant arguments from constructors and branches
irrFun :: MonadTCM m => Fun -> Compile m FunSource
irrExpr :: MonadTCM m => Expr -> Compile m ExprSource
Remove all arguments to constructors that we don't need to store in an expression.
irrBranch :: MonadTCM m => Branch -> Compile m BranchSource
Remove all the arguments that doesn't need to be stored in the constructor For the branch
Produced by Haddock version 2.6.1