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

Agda.Compiler.Agate.UntypedPrinter

Description
Generate GHC code for untyped execution
Documentation

showAsUntypedConstructor :: QName -> TCM Doc | Source

class ShowAsUntypedTerm a where | Source

Methods

showAsUntypedTerm :: a -> TCM Doc | Source

Instances

ShowAsUntypedTerm QName
ShowAsUntypedTerm Name
ShowAsUntypedTerm Term

showUntypedApp :: ShowAsUntypedTerm a => a -> [Arg Term] -> TCM Doc | Source

showUntypedDefinition :: (QName, Definition) -> TCM Doc | Source

untypedAbs :: [Doc] -> Doc -> Doc | Source

showUntypedClause :: Clause -> TCM Doc | Source

Produced by Haddock version 2.4.2