idris

Safe HaskellNone

Idris.Completion

Description

Support for command-line completion at the REPL and in the prover

Synopsis

Documentation

replCompletion :: CompletionFunc IdrisSource

Complete REPL commands and defined identifiers

proverCompletionSource

Arguments

:: [String]

The names of current local assumptions

-> CompletionFunc Idris 

Complete tactics and their arguments