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

class ShowAsOptimizedType a where Source

Methods showAsOptimizedType :: a -> TCM Doc Source

class ShowAsOptimizedTerm a where Source

Methods showAsOptimizedTerm :: a -> TCM Doc Source

Produced by Haddock version 2.6.0