Agda.Compiler.Epic.ConstructorIrrelevancy

Remove forced (irrelevant) arguments from constructors.

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