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 }

@[inline]

def Lake.listToLines {α : Type u_1} (as : List α) (f : α → String) : String

Equations

• Lake.listToLines as f = ((List.foldl (fun (x1 : String) (x2 : α) => toString x1 ++ toString (f x2) ++ toString "\n") "" as).dropEnd 1).copy

@[inline]

def Lake.arrayToLines {α : Type u_1} (as : Array α) (f : α → String) : String

Equations

• Lake.arrayToLines as f = ((Array.foldl (fun (x1 : String) (x2 : α) => toString x1 ++ toString (f x2) ++ toString "\n") "" as).dropEnd 1).copy

instance Lake.instToTextJson : ToText Lean.Json

Equations

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

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

Equations

• Lake.instToTextList = { toText := fun (x : List α) => Lake.listToLines x Lake.toText }

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

Equations

• Lake.instToTextArray = { toText := fun (x : Array α) => Lake.arrayToLines x Lake.toText }

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.instQueryTextList {α : Type u_1} [QueryText α] : QueryText (List α)

Equations

• Lake.instQueryTextList = { queryText := fun (x : List α) => Lake.listToLines x Lake.queryText }

instance Lake.instQueryTextArray {α : Type u_1} [QueryText α] : QueryText (Array α)

Equations

• Lake.instQueryTextArray = { queryText := fun (x : Array α) => Lake.arrayToLines x Lake.queryText }

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.instQueryJsonList {α : Type u_1} [QueryJson α] : QueryJson (List α)

Equations

• Lake.instQueryJsonList = { queryJson := fun (x : List α) => Lean.Json.arr (Array.map Lake.queryJson x.toArray) }

instance Lake.instQueryJsonArray {α : Type u_1} [QueryJson α] : QueryJson (Array α)

Equations

• Lake.instQueryJsonArray = { queryJson := fun (x : Array α) => Lean.Json.arr (Array.map Lake.queryJson x) }

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.