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

Agda.Compiler.Agate.Common

Description
common
Documentation

psep :: [Doc] -> Doc | Source

dropArgs :: Int -> Type -> TCM Type | Source

withFunctionDomain :: Type -> (Type -> TCM a) -> ([a] -> Type -> TCM b) -> TCM b | Source

splitType :: Type -> TCM ([Type], Type) | Source

forEachArgM :: (Type -> TCM a) -> Type -> TCM [a] | Source

underContext :: Type -> TCM a -> TCM a | Source

showOptimizedLiteral :: Literal -> Doc | Source

showUntypedLiteral :: Literal -> Doc | Source

showClause :: (Term -> TCM Doc) -> (QName -> [Doc] -> TCM Doc) -> ([Doc] -> Term -> TCM Doc) -> Clause -> TCM Doc | Source

Produced by Haddock version 2.4.2