Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.HaskellTypes
Description
Translating Agda types to Haskell types. Used to ensure that imported Haskell functions have the right type.
Synopsis
type HaskellKind = String
hsStar :: HaskellKind
hsKFun :: HaskellKind -> HaskellKind -> HaskellKind
hsFun :: HaskellKind -> HaskellKind -> HaskellKind
hsVar :: Name -> HaskellType
hsApp :: String -> [HaskellType] -> HaskellType
hsForall :: String -> HaskellType -> HaskellType
notAHaskellKind :: MonadTCM tcm => Type -> tcm a
notAHaskellType :: MonadTCM tcm => Type -> tcm a
getHsType :: MonadTCM tcm => QName -> tcm HaskellType
getHsVar :: MonadTCM tcm => Nat -> tcm HaskellCode
isHaskellKind :: Type -> TCM Bool
haskellKind :: MonadTCM tcm => Type -> tcm HaskellKind
haskellType :: MonadTCM tcm => Type -> tcm HaskellType
Documentation
type HaskellKind = StringSource
hsStar :: HaskellKindSource
hsKFun :: HaskellKind -> HaskellKind -> HaskellKindSource
hsFun :: HaskellKind -> HaskellKind -> HaskellKindSource
hsVar :: Name -> HaskellTypeSource
hsApp :: String -> [HaskellType] -> HaskellTypeSource
hsForall :: String -> HaskellType -> HaskellTypeSource
notAHaskellKind :: MonadTCM tcm => Type -> tcm aSource
notAHaskellType :: MonadTCM tcm => Type -> tcm aSource
getHsType :: MonadTCM tcm => QName -> tcm HaskellTypeSource
getHsVar :: MonadTCM tcm => Nat -> tcm HaskellCodeSource
isHaskellKind :: Type -> TCM BoolSource
haskellKind :: MonadTCM tcm => Type -> tcm HaskellKindSource
haskellType :: MonadTCM tcm => Type -> tcm HaskellTypeSource

Note that Inf a b, where Inf is the INFINITY builtin, is translated to translation of b (assuming that all coinductive builtins are defined).

Note that if haskellType supported universe polymorphism then the special treatment of INFINITY might not be needed.

Produced by Haddock version 2.6.1