Documentation

Lake.Config.OutFormat

inductive Lake.OutFormat :

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) :

toText : α → String

Instances

@[instance 0]

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

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) :

Class used to format target output for lake query.

formatQuery : OutFormat → α → String

Instances

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} :

Equations

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

@[specialize #[]]

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

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 α] :

Equations

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

instance Lake.instFormatQueryUnit :

FormatQuery Unit

Equations

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