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.

@[deprecated Lake.QueryText (since := "2025-07-25")]

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.QueryText (α : Type u) : Type u

Class used to format target output as text for lake query.

• queryText : α → String

  Format target output as text (e.g., for lake query).

@[instance 0]

instance Lake.instQueryText {α : Type u_1} : QueryText α

Equations

• Lake.instQueryText = { queryText := fun (x : α) => "" }

@[instance 100]

instance Lake.instQueryTextOfToText {α : Type u_1} [ToText α] : QueryText α

Equations

• Lake.instQueryTextOfToText = { queryText := Lake.toText }

instance Lake.instQueryTextUnit : QueryText Unit

Equations

• Lake.instQueryTextUnit = { queryText := fun (x : Unit) => "" }

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

Class used to format target output as JSON for lake query -J.

• queryJson : α → Lean.Json

  Format target output as JSON (e.g., for lake query -J).

@[instance 0]

instance Lake.instQueryJson {α : Type u_1} : QueryJson α

Equations

• Lake.instQueryJson = { queryJson := fun (x : α) => Lean.Json.null }

@[instance 100]

instance Lake.instQueryJsonOfToJson {α : Type u_1} [Lean.ToJson α] : QueryJson α

Equations

• Lake.instQueryJsonOfToJson = { queryJson := Lean.toJson }

instance Lake.instQueryJsonUnit : QueryJson Unit

Equations

• Lake.instQueryJsonUnit = { queryJson := fun (x : Unit) => Lean.Json.null }

class Lake.FormatQuery (α : Type u) extends Lake.QueryText α, Lake.QueryJson α : Type u

Class used to format target output for lake query.

• queryText : α → String
• queryJson : α → Lean.Json

instance Lake.instFormatQueryOfQueryTextOfQueryJson {α : Type u_1} [QueryText α] [QueryJson α] : FormatQuery α

Equations

• Lake.instFormatQueryOfQueryTextOfQueryJson = { toQueryText := inst✝¹, toQueryJson := inst✝ }

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

Format function that produces "null" output.

Equations

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

@[specialize #[]]

def Lake.formatQuery {α : Type u_1} [FormatQuery α] (fmt : OutFormat) (a : α) : String

Format function that uses QueryText and QueryJson to produce output.

Equations

• Lake.formatQuery Lake.OutFormat.text a = Lake.queryText a
• Lake.formatQuery Lake.OutFormat.json a = (Lake.queryJson a).compress

def Lake.ppImport (imp : Lean.Import) (isModule : Bool) (init : String := "") : String

Equations

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

def Lake.ppModuleHeader (header : Lean.ModuleHeader) : String

Equations

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

instance Lake.instQueryTextModuleHeader : QueryText Lean.ModuleHeader

Equations

• Lake.instQueryTextModuleHeader = { queryText := Lake.ppModuleHeader }