| Safe Haskell | None |
|---|
Idris.Completion
Description
Support for command-line completion at the REPL and in the prover
- replCompletion :: CompletionFunc Idris
- proverCompletion :: [String] -> CompletionFunc Idris
Documentation
replCompletion :: CompletionFunc IdrisSource
Complete REPL commands and defined identifiers
Arguments
| :: [String] | The names of current local assumptions |
| -> CompletionFunc Idris |
Complete tactics and their arguments