def Lake.Reservoir.lakeHeaders : Array String

Equations

• Lake.Reservoir.lakeHeaders = #["X-Reservoir-Api-Version:1.0.0", "X-Lake-Registry-Api-Version:0.1.0"]

inductive Lake.ReservoirResp (α : Type u) : Type u

A Reservoir API response object.

• data {α : Type u} (a : α) : ReservoirResp α
• error {α : Type u} (status : Nat) (message : String) : ReservoirResp α

def Lake.ReservoirResp.fromJson? {α : Type} [Lean.FromJson α] (val : Lean.Json) : Except String (ReservoirResp α)

Equations

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

@[implicit_reducible]

instance Lake.instFromJsonReservoirResp {α : Type} [Lean.FromJson α] : Lean.FromJson (ReservoirResp α)

Equations

• Lake.instFromJsonReservoirResp = { fromJson? := Lake.ReservoirResp.fromJson? }