Safe Haskell	None
Language	Haskell2010

Idris.REPL.Commands

Synopsis

Documentation

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)
RunShellCommand FilePath
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]
Verbosity Int
Spec PTerm
WHNF PTerm
TestInline PTerm
Defn Name
Missing Name
DynamicLink FilePath
ListDynamic
Pattelab PTerm
Search [PkgName] 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 [PkgName] String
WhoCalls Name
CallsWho Name
Browse [String]
MakeDoc String
ShowVersion
Warranty
PrintDef Name
PPrint OutputFmt Int PTerm
TransformInfo Name
DebugInfo Name
DebugUnify PTerm PTerm