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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.MAlonzo.HaskellTypes

Description

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

Documentation

haskellType :: QName -> TCM Type Source #

checkConstructorCount :: QName -> [QName] -> [HaskellCode] -> TCM () Source #

hsTelApproximation :: Type -> TCM ([Type], Type) Source #

hsTelApproximation' :: PolyApprox -> Type -> TCM ([Type], Type) Source #