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

Safe HaskellNone
LanguageHaskell98

Agda.Compiler.Epic.ForceConstrs

Description

Remove forced arguments from constructors.

Synopsis

Documentation

makeForcedArgs :: Type -> ForcedArgs Source

Check which arguments are forced

forceConstrs :: [Fun] -> Compile TCM [Fun] Source

Remove forced arguments from constructors and branches

forceFun :: Fun -> Compile TCM Fun Source