Idris.REPL.Commands

Synopsis

• data Command
  • = Quit
  • | Help
  • | Eval PTerm
  • | NewDefn [PDecl]
  • | 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
  • | 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 [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

Documentation