Idris2Doc : TTImp.Interactive.Completion

TTImp.Interactive.Completion

(source)

Definitions

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

Visibility: export