Agda-2.2.10: A dependently typed functional programming language and proof assistant

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 -> IrrFilter

Check which arguments are forced and create an IrrFilter

constrIrr :: MonadTCM m => [Fun] -> Compile m [Fun]

Remove irrelevant arguments from constructors and branches

irrFun :: MonadTCM m => Fun -> Compile m Fun

irrExpr :: MonadTCM m => Expr -> Compile m Expr

Remove all arguments to constructors that we don't need to store in an expression.

irrBranch :: MonadTCM m => Branch -> Compile m Branch

Remove all the arguments that doesn't need to be stored in the constructor For the branch