inductive Lake.CliError : Type

• missingCommand: Lake.CliError
• unknownCommand: String → Lake.CliError
• missingArg: String → Lake.CliError
• missingOptArg: String → String → Lake.CliError
• invalidOptArg: String → String → Lake.CliError
• unknownShortOption: Char → Lake.CliError
• unknownLongOption: String → Lake.CliError
• unexpectedArguments: List String → Lake.CliError
• unknownTemplate: String → Lake.CliError
• unknownConfigLang: String → Lake.CliError
• unknownModule: Lean.Name → Lake.CliError
• unknownPackage: String → Lake.CliError
• unknownFacet: String → Lean.Name → Lake.CliError
• unknownTarget: Lean.Name → Lake.CliError
• missingModule: Lean.Name → Lean.Name → Lake.CliError
• missingTarget: Lean.Name → String → Lake.CliError
• nonCliTarget: Lean.Name → Lake.CliError
• nonCliFacet: String → Lean.Name → Lake.CliError
• invalidTargetSpec: String → Char → Lake.CliError
• invalidFacet: Lean.Name → Lean.Name → Lake.CliError
• unknownExe: String → Lake.CliError
• unknownScript: String → Lake.CliError
• missingScriptDoc: String → Lake.CliError
• invalidScriptSpec: String → Lake.CliError
• outputConfigExists: System.FilePath → Lake.CliError

  Translate Errors

• unknownLeanInstall: Lake.CliError
• unknownLakeInstall: Lake.CliError
• leanRevMismatch: String → String → Lake.CliError
• invalidEnv: 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 }