Agda-2.2.6: 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.
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
Produced by Haddock version 2.4.2