idris-1.3.1: Functional Programming Language with Dependent Types

License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.Completion

Description

Synopsis

replCompletion :: CompletionFunc Idris
proverCompletion :: [String] -> CompletionFunc Idris

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