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

Agda.Compiler.Agate.OptimizedPrinter

Description
Generate GHC code for optimized datatypes and their values
Documentation

showAsOptimizedConstructor :: QName -> TCM Doc | Source

showOptimizedDefinitions :: Definitions -> TCM () | Source

showTypeDeclarations :: Definitions -> [QName] -> TCM Doc | Source

showTypeDeclaration :: Definitions -> QName -> TCM Doc | Source

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

underDatatypeParameters :: Nat -> Type -> (Doc -> Type -> TCM (a -> a)) -> (Type -> TCM a) -> TCM a | Source

showValueDefinitions :: Definitions -> [QName] -> TCM Doc | Source

showValueDefinition :: Definitions -> [QName] -> (QName, Definition) -> TCM Doc | Source

showOptimizedClause :: Doc -> Clause -> TCM Doc | Source

class ShowAsOptimizedKind a where | Source

Methods

showAsOptimizedKind :: a -> TCM Doc | Source

Instances

ShowAsOptimizedKind Type
ShowAsOptimizedKind Term

class ShowAsOptimizedType a where | Source

Methods

showAsOptimizedType :: a -> TCM Doc | Source

Instances

ShowAsOptimizedType QName
ShowAsOptimizedType Type
ShowAsOptimizedType Term

class ShowAsOptimizedTerm a where | Source

Methods

showAsOptimizedTerm :: a -> TCM Doc | Source

Instances

ShowAsOptimizedTerm QName
ShowAsOptimizedTerm Name
ShowAsOptimizedTerm Term

Produced by Haddock version 2.4.2