Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Compiler.HaskellTypes
Description
Translating Agda types to Haskell types. Used to ensure that imported Haskell functions have the right type.
Documentation
type
HaskellKind
=
String
Source
hsStar
::
HaskellKind
Source
hsKFun
::
HaskellKind
->
HaskellKind
->
HaskellKind
Source
hsFun
::
HaskellKind
->
HaskellKind
->
HaskellKind
Source
hsVar
::
Name
->
HaskellType
Source
hsApp
::
String
-> [
HaskellType
] ->
HaskellType
Source
hsForall
::
String
->
HaskellType
->
HaskellType
Source
notAHaskellKind
::
MonadTCM
tcm =>
Type
-> tcm a
Source
notAHaskellType
::
MonadTCM
tcm =>
Type
-> tcm a
Source
getHsType
::
MonadTCM
tcm =>
QName
-> tcm
HaskellType
Source
getHsVar
::
MonadTCM
tcm =>
Nat
-> tcm
HaskellCode
Source
isHaskellKind
::
Type
->
TCM
Bool
Source
haskellKind
::
MonadTCM
tcm =>
Type
-> tcm
HaskellKind
Source
haskellType
::
MonadTCM
tcm =>
Type
-> tcm
HaskellType
Source
Produced by
Haddock
version 2.6.0