Idris.REPL.Commands

Documentation

data Command

REPL commands

Constructors

Quit

Help

Eval PTerm

NewDefn [PDecl]

Each PDecl should be either a type declaration (at most one) or a clause defining the same name.

Undefine [Name]

Check PTerm

Core PTerm

DocStr (Either Name Const) HowMuchDocs

TotCheck Name

Reload

Watch

Load FilePath (Maybe Int)

ChangeDirectory FilePath

ModImport String

Edit

Compile Codegen String

Execute PTerm

ExecVal PTerm

Metavars

Prove Bool Name

If false, use prover, if true, use elab shell

AddProof (Maybe Name)

RmProof Name

ShowProof Name

Proofs

Universes

LogLvl Int

LogCategory [LogCat]

Spec PTerm

WHNF PTerm

TestInline PTerm

Defn Name

Missing Name

DynamicLink FilePath

ListDynamic

Pattelab PTerm

Search [String] PTerm

CaseSplitAt Bool Int Name

AddClauseFrom Bool Int Name

AddProofClauseFrom Bool Int Name

AddMissing Bool Int Name

MakeWith Bool Int Name

MakeCase Bool Int Name

MakeLemma Bool Int Name

DoProofSearch Bool Bool Int Name [Name]

SetOpt Opt

UnsetOpt Opt

NOP

SetColour ColourType IdrisColour

ColourOn

ColourOff

ListErrorHandlers

SetConsoleWidth ConsoleWidth

SetPrinterDepth (Maybe Int)

Apropos [String] String

WhoCalls Name

CallsWho Name

Browse [String]

MakeDoc String

Warranty

PrintDef Name

PPrint OutputFmt Int PTerm

TransformInfo Name

DebugInfo Name

DebugUnify PTerm PTerm