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

Agda.Compiler.Agate.Common

Description

common

Documentation

psep :: [Doc] -> DocSource

dropArgs :: Int -> Type -> TCM TypeSource

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

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

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

underContext :: Type -> TCM a -> TCM aSource

showOptimizedLiteral :: Literal -> DocSource

showUntypedLiteral :: Literal -> DocSource

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