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

Agda.Compiler.Agate.OptimizedPrinter

Description

Generate GHC code for optimized datatypes and their values

Documentation

showAsOptimizedConstructor :: QName -> TCM DocSource

showOptimizedDefinitions :: Definitions -> TCM ()Source

showTypeDeclarations :: Definitions -> [QName] -> TCM DocSource

showTypeDeclaration :: Definitions -> QName -> TCM DocSource

showTypeParameter :: Doc -> Type -> TCM ([Doc] -> [Doc])Source

underDatatypeParameters :: Nat -> Type -> (Doc -> Type -> TCM (a -> a)) -> (Type -> TCM a) -> TCM aSource

showValueDefinitions :: Definitions -> [QName] -> TCM DocSource

showValueDefinition :: Definitions -> [QName] -> (QName, Definition) -> TCM DocSource

showOptimizedClause :: Doc -> Clause -> TCM DocSource

class ShowAsOptimizedKind a whereSource

Methods

showAsOptimizedKind :: a -> TCM DocSource

Instances

class ShowAsOptimizedType a whereSource

Methods

showAsOptimizedType :: a -> TCM DocSource

Instances

class ShowAsOptimizedTerm a whereSource

Methods

showAsOptimizedTerm :: a -> TCM DocSource

Instances