idris-1.3.4: Functional Programming Language with Dependent Types
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.REPL.Commands

Synopsis

Documentation

data Command Source #

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