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

Safe HaskellSafe-Infered

Agda.Compiler.MAlonzo.Primitives

Synopsis

Documentation

checkTypeOfMain :: QName -> Type -> TCM ()Source

Check that the main function has type IO a, for some a.

xForPrim :: [(String, TCM [a])] -> TCM [a]Source

repl :: [[Char]] -> [Char] -> [Char]Source