Protocol.IDE.Command

Definitions

data DocMode : Type

Totality: total
Visibility: public export
Constructors:

Overview : DocMode

Full : DocMode

record Hints : Type

Totality: total
Visibility: public export
Constructor: 

MkHints : List String -> Hints

Projection: 

.list : Hints -> List String

Hints:

FromSExpable Hints

SExpable Hints

.list : Hints -> List String

Totality: total
Visibility: public export

list : Hints -> List String

Totality: total
Visibility: public export

data IDECommand : Type

Totality: total
Visibility: public export
Constructors:

Interpret : String -> IDECommand

LoadFile : String -> Maybe Integer -> IDECommand

TypeOf : String -> Maybe (Integer, Integer) -> IDECommand

NameAt : String -> Maybe (Integer, Integer) -> IDECommand

CaseSplit : Integer -> Integer -> String -> IDECommand

AddClause : Integer -> String -> IDECommand

AddMissing : Integer -> String -> IDECommand

Intro : Integer -> String -> IDECommand

Refine : Integer -> String -> String -> IDECommand

ExprSearch : Integer -> String -> Hints -> Bool -> IDECommand

ExprSearchNext : IDECommand

GenerateDef : Integer -> String -> IDECommand

GenerateDefNext : IDECommand

MakeLemma : Integer -> String -> IDECommand

MakeCase : Integer -> String -> IDECommand

MakeWith : Integer -> String -> IDECommand

DocsFor : String -> Maybe DocMode -> IDECommand

Directive : String -> IDECommand

Apropos : String -> IDECommand

Metavariables : Integer -> IDECommand

WhoCalls : String -> IDECommand

CallsWho : String -> IDECommand

BrowseNamespace : String -> IDECommand

NormaliseTerm : String -> IDECommand

ShowTermImplicits : String -> IDECommand

HideTermImplicits : String -> IDECommand

ElaborateTerm : String -> IDECommand

PrintDefinition : String -> IDECommand

ReplCompletions : String -> IDECommand

EnableSyntax : Bool -> IDECommand

Version : IDECommand

GetOptions : IDECommand

Hints:

FromSExpable IDECommand

SExpable IDECommand