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

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 aSource

notAHaskellType :: MonadTCM tcm => Type -> tcm aSource

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