inductive Lake.CliError : Type

• missingCommand: Lake.CliError
• unknownCommand: String → Lake.CliError
• missingArg: String → Lake.CliError
• missingOptArg: 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: Lake.Name → Lake.CliError
• unknownPackage: String → Lake.CliError
• unknownFacet: String → Lake.Name → Lake.CliError
• unknownTarget: Lake.Name → Lake.CliError
• missingModule: Lake.Name → Lake.Name → Lake.CliError
• missingTarget: Lake.Name → String → Lake.CliError
• nonCliTarget: Lake.Name → Lake.CliError
• nonCliFacet: String → Lake.Name → Lake.CliError
• invalidTargetSpec: String → Char → Lake.CliError
• invalidFacet: Lake.Name → Lake.Name → Lake.CliError
• unknownExe: String → Lake.CliError
• unknownScript: String → Lake.CliError
• missingScriptDoc: String → Lake.CliError
• invalidScriptSpec: String → Lake.CliError
• outputConfigExists: Lake.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.

instance Lake.CliError.instToString : ToString Lake.CliError

Equations

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