Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

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 Source

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 Fun Source

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

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

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

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

Produced by Haddock version 2.6.1