TTImp.Elab.ImplicitBind

Definitions

mkOuterHole : Ref EST (EState vars) => Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Name -> Env Term vars -> Maybe (Glued vars) -> Core (Term vars, Term vars)

Visibility: export

mkPatternHole : Ref EST (EState vars') => Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Name -> Env Term vars' -> BindMode -> Maybe (Glued vars') -> Core (Term vars', (Term vars', Term vars'))

Visibility: export

normaliseType : Ref Ctxt Defs => Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

bindImplicits : FC -> BindMode -> Defs -> Env Term vars -> List (Name, ImplBinding vars) -> Term vars -> Term vars -> Core (Term vars, Term vars)

Visibility: export

implicitBind : Ref Ctxt Defs => Ref UST UState => Name -> Core ()

Visibility: export

getToBind : Ref Ctxt Defs => Ref EST (EState vars) => Ref UST UState => FC -> ElabMode -> BindMode -> Env Term vars -> List Name -> Core (List (Name, ImplBinding vars))

Visibility: export

checkBindVar : 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 -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

checkBindHere : 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 -> BindMode -> RawImp -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export