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

Agda.Compiler.Agate.UntypedPrinter

Description

Generate GHC code for untyped execution

Documentation

showAsUntypedConstructor :: QName -> TCM Doc Source

class ShowAsUntypedTerm a whereSource

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