inductive Lake.CliError : Type

• missingCommand : CliError
• unknownCommand (cmd : String) : CliError
• missingArg (arg : String) : CliError
• missingOptArg (opt arg : String) : CliError
• invalidOptArg (opt arg : String) : CliError
• unknownShortOption (opt : Char) : CliError
• unknownLongOption (opt : String) : CliError
• unexpectedArguments (args : List String) : CliError
• unexpectedPlus : CliError
• unknownTemplate (spec : String) : CliError
• unknownConfigLang (spec : String) : CliError
• unknownModule (mod : Lean.Name) : CliError
• unknownModulePath (path : System.FilePath) : CliError
• unknownPackage (spec : String) : CliError
• unknownFacet (type : String) (facet : Lean.Name) : CliError
• unknownTarget (target : Lean.Name) : CliError
• missingModule (pkg mod : Lean.Name) : CliError
• missingTarget (pkg : Lean.Name) (spec : String) : CliError
• invalidBuildTarget (key : String) : CliError
• invalidTargetSpec (spec : String) (tooMany : Char) : CliError
• invalidFacet (target facet : Lean.Name) : CliError
• unknownExe (spec : String) : CliError
• unknownScript (script : String) : CliError
• missingScriptDoc (script : String) : CliError
• invalidScriptSpec (spec : String) : CliError
• outputConfigExists (path : System.FilePath) : CliError

  Translate Errors

• unknownLeanInstall : CliError
• unknownLakeInstall : CliError
• leanRevMismatch (expected actual : String) : CliError
• invalidEnv (msg : String) : CliError
• missingRootDir (path : System.FilePath) : CliError

instance Lake.instInhabitedCliError : Inhabited CliError

Equations

• Lake.instInhabitedCliError = { default := Lake.CliError.missingCommand }

instance Lake.instReprCliError : Repr CliError

Equations

• Lake.instReprCliError = { reprPrec := Lake.reprCliError✝ }

def Lake.CliError.toString : CliError → String

Equations

• One or more equations did not get rendered due to their size.
• Lake.CliError.missingCommand.toString = "missing command"
• (Lake.CliError.unknownCommand a).toString = toString "unknown command '" ++ toString a ++ toString "'"
• (Lake.CliError.missingArg a).toString = toString "missing " ++ toString a ++ toString ""
• (Lake.CliError.missingOptArg a a_1).toString = toString "missing " ++ toString a_1 ++ toString " for " ++ toString a ++ toString ""
• (Lake.CliError.invalidOptArg a a_1).toString = toString "invalid argument for " ++ toString a ++ toString "; expected " ++ toString a_1 ++ toString ""
• (Lake.CliError.unknownShortOption a).toString = toString "unknown short option '-" ++ toString a ++ toString "'"
• (Lake.CliError.unknownLongOption a).toString = toString "unknown long option '" ++ toString a ++ toString "'"
• (Lake.CliError.unexpectedArguments a).toString = toString "unexpected arguments: " ++ toString (" ".intercalate a) ++ toString ""
• Lake.CliError.unexpectedPlus.toString = toString "the `+` option is an Elan feature; rerun Lake via Elan and ensure this option comes first."
• (Lake.CliError.unknownTemplate a).toString = toString "unknown package template `" ++ toString a ++ toString "`"
• (Lake.CliError.unknownConfigLang a).toString = toString "unknown configuration language `" ++ toString a ++ toString "`"
• (Lake.CliError.unknownModule a).toString = toString "unknown module `" ++ toString (a.toString false) ++ toString "`"
• (Lake.CliError.unknownModulePath a).toString = toString "unknown module source path `" ++ toString a ++ toString "`"
• (Lake.CliError.unknownPackage a).toString = toString "unknown package `" ++ toString a ++ toString "`"
• (Lake.CliError.unknownFacet a a_1).toString = toString "unknown " ++ toString a ++ toString " facet `" ++ toString (a_1.toString false) ++ toString "`"
• (Lake.CliError.unknownTarget a).toString = toString "unknown target `" ++ toString (a.toString false) ++ toString "`"
• (Lake.CliError.missingModule a a_1).toString = toString "package '" ++ toString (a.toString false) ++ toString "' has no module '" ++ toString (a_1.toString false) ++ toString "'"
• (Lake.CliError.missingTarget a a_1).toString = toString "package '" ++ toString (a.toString false) ++ toString "' has no target '" ++ toString a_1 ++ toString "'"
• (Lake.CliError.invalidBuildTarget a).toString = toString "'" ++ toString a ++ toString "' is not a build target (perhaps you meant 'lake query'?)"
• (Lake.CliError.invalidTargetSpec a a_1).toString = toString "invalid target specifier '" ++ toString a ++ toString "' (too many '" ++ toString a_1 ++ toString "')"
• (Lake.CliError.invalidFacet a a_1).toString = toString "invalid facet `" ++ toString (a_1.toString false) ++ toString "`; target " ++ toString (a.toString false) ++ toString " has no facets"
• (Lake.CliError.unknownExe a).toString = toString "unknown executable " ++ toString a ++ toString ""
• (Lake.CliError.unknownScript a).toString = toString "unknown script " ++ toString a ++ toString ""
• (Lake.CliError.missingScriptDoc a).toString = toString "no documentation provided for `" ++ toString a ++ toString "`"
• (Lake.CliError.invalidScriptSpec a).toString = toString "invalid script specifier '" ++ toString a ++ toString "' (too many '/')"
• (Lake.CliError.outputConfigExists a).toString = toString "output configuration file already exists: " ++ toString a ++ toString ""
• Lake.CliError.unknownLeanInstall.toString = "could not detect a Lean installation"
• Lake.CliError.unknownLakeInstall.toString = "could not detect the configuration of the Lake installation"
• (Lake.CliError.invalidEnv a).toString = a
• (Lake.CliError.missingRootDir a).toString = toString "workspace directory not found: " ++ toString a ++ toString ""

instance Lake.CliError.instToString : ToString CliError

Equations

• Lake.CliError.instToString = { toString := Lake.CliError.toString }