Idris2Doc : TTImp.Interactive.Completion

TTImp.Interactive.Completion

(source)

Definitions

completion : Ref Ctxt Defs => String -> Core (Maybe (String, List String))
  Completion receives the full line and returns
1. the ignored prefix
2. the list of possible completions

Visibility: export