idris-0.10.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Completion

Description

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

Synopsis

Documentation

replCompletion :: CompletionFunc Idris Source

Complete REPL commands and defined identifiers

proverCompletion Source

Arguments

:: [String]

The names of current local assumptions

-> CompletionFunc Idris 

Complete tactics and their arguments