inductive Lake.OutFormat : Type

Target output formats supported by the Lake CLI (e.g., lake query).

• text : OutFormat

  Format target output as text.

• json : OutFormat

  Format target output as JSON.

class Lake.ToText (α : Type u) : Type u

• toText : α → String

@[instance 0]

instance Lake.instToTextOfToString {α : Type u_1} [ToString α] : ToText α

instance Lake.instToTextJson : ToText Lean.Json

instance Lake.instToTextList {α : Type u_1} [ToText α] : ToText (List α)

instance Lake.instToTextArray {α : Type u_1} [ToText α] : ToText (Array α)

class Lake.FormatQuery (α : Type u) : Type u

Class used to format target output for lake query.

• formatQuery : OutFormat → α → String

def Lake.nullFormat {α : Sort u_1} (fmt : OutFormat) : α → String

A format function that produces "null" output.

@[instance 0]

instance Lake.instFormatQuery {α : Type u_1} : FormatQuery α

@[specialize #[]]

def Lake.stdFormat {α : Type u_1} [ToText α] [Lean.ToJson α] (fmt : OutFormat) (a : α) : String

Format function that uses ToText and ToJson to print output.

instance Lake.instFormatQueryOfToTextOfToJson {α : Type u_1} [ToText α] [Lean.ToJson α] : FormatQuery α

instance Lake.instFormatQueryUnit : FormatQuery Unit