inductive Lake.CliError : Type

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

  Translate Errors

• unknownLeanInstall : Lake.CliError
• unknownLakeInstall : Lake.CliError
• leanRevMismatch (expected actual : String) : Lake.CliError
• invalidEnv (msg : String) : Lake.CliError

instance Lake.instInhabitedCliError : Inhabited Lake.CliError

Equations

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

instance Lake.instReprCliError : Repr Lake.CliError

Equations

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

def Lake.CliError.toString : Lake.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.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.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.nonCliTarget a).toString = toString "target `" ++ toString (a.toString false) ++ toString "` is not a buildable via `lake`"
• (Lake.CliError.nonCliFacet a a_1).toString = toString "" ++ toString a ++ toString " facet `" ++ toString (a_1.toString false) ++ toString "` is not a buildable via `lake`"
• (Lake.CliError.invalidTargetSpec a a_1).toString = toString "invalid script spec '" ++ 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 spec '" ++ 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

instance Lake.CliError.instToString : ToString Lake.CliError

Equations

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