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 α

@[inline]

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

@[inline]

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

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.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 α

@[instance 100]

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

instance Lake.instQueryTextList {α : Type u_1} [QueryText α] : QueryText (List α)

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

instance Lake.instQueryTextUnit : QueryText 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 α

@[instance 100]

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

instance Lake.instQueryJsonList {α : Type u_1} [QueryJson α] : QueryJson (List α)

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

instance Lake.instQueryJsonUnit : QueryJson Unit

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 α

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

Format function that produces "null" output.

@[specialize #[]]

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

Format function that uses QueryText and QueryJson to produce output.

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

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