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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.HaskellTypes

Description

Translating Agda types to Haskell types. Used to ensure that imported Haskell functions have the right type.

Synopsis

Documentation

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.