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

Safe HaskellNone

Agda.Compiler.JS.Compiler

Documentation

compilerMain :: Interface -> TCM ()Source

compile :: Interface -> TCM ()Source

prefix :: [Char]Source

jsMod :: ModuleName -> GlobalIdSource

jsFileName :: GlobalId -> StringSource

jsMember :: Name -> MemberIdSource

global' :: QName -> TCM (Exp, [MemberId])Source

global :: QName -> TCM (Exp, [MemberId])Source

reorder :: [Export] -> [Export]Source

reorder' :: Set [MemberId] -> [Export] -> [Export]Source

isTopLevelValue :: Export -> BoolSource

isEmptyObject :: Export -> BoolSource

insertAfter :: Set [MemberId] -> Export -> [Export] -> [Export]Source

curModule :: TCM ModuleSource

definition :: (QName, Definition) -> TCM ExportSource

defn :: QName -> [MemberId] -> Type -> Maybe JSCode -> Defn -> TCM ExpSource

numPars :: [Clause] -> NatSource

clause :: Clause -> TCM CaseSource

mapping :: [Pattern] -> (Nat, Nat, [Exp])Source

mapping' :: Pattern -> (Nat, Nat, [Exp]) -> (Nat, Nat, [Exp])Source

pattern :: Pattern -> TCM PattSource

tag :: QName -> TCM TagSource

visitorName :: QName -> TCM MemberIdSource

body :: ClauseBody -> TCM ExpSource

term :: Term -> TCM ExpSource

isSingleton :: Type -> TCM (Maybe Exp)Source

args :: Int -> Args -> TCM [Exp]Source

qname :: QName -> TCM ExpSource

literal :: Literal -> ExpSource

dummyLambda :: Int -> Exp -> ExpSource

writeModule :: Module -> TCM ()Source

compileDir :: TCM FilePathSource

outFile :: GlobalId -> TCM FilePathSource

outFile_ :: TCM FilePathSource