Translating Agda types to Haskell types. Used to ensure that imported Haskell functions have the right type.
- 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
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.