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

Agda.Compiler.JS.Compiler

Documentation

compilerMain :: Interface -> TCM ()Source

compile :: Interface -> TCM ()Source

jsMod :: ModuleName -> GlobalId Source

jsFileName :: GlobalId -> String Source

jsMember :: Name -> MemberId Source

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

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

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

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

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

curModule :: TCM Module Source

definition :: (QName, Definition) -> TCM Export Source

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

numPars :: [Clause] -> Nat Source

clause :: Clause -> TCM Case Source

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

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

pattern :: Pattern -> TCM Patt Source

tag :: QName -> TCM Tag Source

visitorName :: QName -> TCM MemberId Source

body :: ClauseBody -> TCM Exp Source

term :: Term -> TCM Exp Source

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

defProjection :: Definition -> Maybe (QName, Int)Source

args :: Maybe (QName, Int) -> Args -> TCM [Exp]Source

qname :: QName -> TCM Exp Source

literal :: Literal -> Exp Source

dummyLambda :: Int -> Exp -> Exp Source

writeModule :: Module -> TCM ()Source

compileDir :: TCM FilePath Source

outFile :: GlobalId -> TCM FilePath Source

outFile_ :: TCM FilePath Source