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



Remove forced (irrelevant) arguments from constructors.



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

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