Agda.Compiler.Common

Documentation

data IsMain

Constructors

IsMain

NotMain

Instances

Eq IsMain

Defined in Agda.Compiler.Common

Methods

(==) :: IsMain -> IsMain -> Bool

(/=) :: IsMain -> IsMain -> Bool

Show IsMain

Defined in Agda.Compiler.Common

Methods

showsPrec :: Int -> IsMain -> ShowS

show :: IsMain -> String

showList :: [IsMain] -> ShowS

Semigroup IsMain

Conjunctive semigroup (NotMain is absorbing).

Defined in Agda.Compiler.Common

Methods

(<>) :: IsMain -> IsMain -> IsMain

sconcat :: NonEmpty IsMain -> IsMain

stimes :: Integral b => b -> IsMain -> IsMain

Monoid IsMain

Defined in Agda.Compiler.Common

Methods

mempty :: IsMain

mappend :: IsMain -> IsMain -> IsMain

mconcat :: [IsMain] -> IsMain

doCompile :: forall r. Monoid r => IsMain -> Interface -> (IsMain -> Interface -> TCM r) -> TCM r

setInterface :: Interface -> TCM ()

curIF :: TCM Interface

curSig :: TCM Signature

curMName :: TCM ModuleName

curDefs :: TCM Definitions

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

sigMName :: Signature -> ModuleName

compileDir :: TCM FilePath

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

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

Sets up the compilation environment.

topLevelModuleName :: ModuleName -> TCM ModuleName