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

instance Lake.CliError.instToString : ToString Lake.CliError