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
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.6.0