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

Safe HaskellNone
LanguageHaskell98

Agda.Compiler.Common

Synopsis

Documentation

data IsMain Source

Constructors

IsMain 
NotMain 

Instances

doCompile :: IsMain -> Interface -> (IsMain -> Interface -> TCM ()) -> TCM () Source

setInterface :: Interface -> TCM () Source

curIF :: TCM Interface Source

curSig :: TCM Signature Source

curMName :: TCM ModuleName Source

curDefs :: TCM Definitions Source

sortDefs :: Definitions -> [(QName, Definition)] Source

sigMName :: Signature -> ModuleName Source

compileDir :: TCM FilePath Source

repl :: [String] -> String -> String Source

conArityAndPars :: QName -> TCM (Nat, Nat) Source

Copy pasted from MAlonzo.... Move somewhere else!

inCompilerEnv :: Interface -> TCM a -> TCM a Source

Sets up the compilation environment.

topLevelModuleName :: ModuleName -> TCM ModuleName Source