TTImp.Elab.Local

Definitions

localHelper : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => NestedNames vars -> Env Term vars -> List ImpDecl -> (NestedNames vars -> Core a) -> Core a

Visibility: export

checkLocal : 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 -> List ImpDecl -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

checkCaseLocal : 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 -> Name -> Name -> List Name -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export