Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- hsUnit :: HaskellType
- hsVar :: Name -> HaskellType
- hsApp :: String -> [HaskellType] -> HaskellType
- hsForall :: String -> HaskellType -> HaskellType
- notAHaskellType :: Type -> TCM a
- getHsType :: QName -> TCM HaskellType
- getHsVar :: Nat -> TCM HaskellCode
- haskellType' :: Type -> TCM HaskellType
- haskellType :: QName -> TCM HaskellType
- checkConstructorCount :: QName -> [QName] -> [HaskellCode] -> TCM ()
Documentation
type HaskellKind = String Source #
hsStar :: HaskellKind Source #
hsKFun :: HaskellKind -> HaskellKind -> HaskellKind Source #
hsFun :: HaskellKind -> HaskellKind -> HaskellKind Source #
hsUnit :: HaskellType Source #
hsVar :: Name -> HaskellType Source #
hsApp :: String -> [HaskellType] -> HaskellType Source #
hsForall :: String -> HaskellType -> HaskellType Source #
notAHaskellType :: Type -> TCM a Source #
haskellType' :: Type -> TCM HaskellType Source #
Note that Inf a b
, where Inf
is the INFINITY builtin, is
translated to 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.
haskellType :: QName -> TCM HaskellType Source #
checkConstructorCount :: QName -> [QName] -> [HaskellCode] -> TCM () Source #