TTImp.Elab.RunElab

Definitions

elabScript : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => RigCount -> FC -> NestedNames vars -> Env Term vars -> NF vars -> Maybe (Glued vars) -> Core (NF vars)

Visibility: export

checkRunElab : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> FC -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export