TTImp.Elab

Definitions

normaliseHoleTypes : Ref Ctxt Defs => Ref UST UState => Core ()

Visibility: export

addHoleToSave : Ref Ctxt Defs => Name -> Core ()

Visibility: export

elabTermSub : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => Int -> ElabMode -> List ElabOpt -> NestedNames vars -> Env Term vars -> Env Term inner -> Thin inner vars -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

elabTerm : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => Int -> ElabMode -> List ElabOpt -> NestedNames vars -> Env Term vars -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

checkTermSub : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => Int -> ElabMode -> List ElabOpt -> NestedNames vars -> Env Term vars -> Env Term inner -> Thin inner vars -> RawImp -> Glued vars -> Core (Term vars)

Visibility: export

checkTerm : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => Int -> ElabMode -> List ElabOpt -> NestedNames vars -> Env Term vars -> RawImp -> Glued vars -> Core (Term vars)

Visibility: export