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