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 α

Equations

• Lake.instToTextOfToString = { toText := toString }

instance Lake.instToTextJson : ToText Lean.Json

Equations

• Lake.instToTextJson = { toText := Lean.Json.compress }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lake.nullFormat Lake.OutFormat.text x✝ = ""
• Lake.nullFormat Lake.OutFormat.json x✝ = Lean.Json.null.compress

@[instance 0]

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

Equations

• Lake.instFormatQuery = { formatQuery := Lake.nullFormat }

@[specialize #[]]

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

Format function that uses ToText and ToJson to print output.

Equations

• Lake.stdFormat Lake.OutFormat.text a = Lake.toText a
• Lake.stdFormat Lake.OutFormat.json a = (Lean.toJson a).compress

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

Equations

• Lake.instFormatQueryOfToTextOfToJson = { formatQuery := Lake.stdFormat }

instance Lake.instFormatQueryUnit : FormatQuery Unit

Equations

• Lake.instFormatQueryUnit = { formatQuery := Lake.nullFormat }