Documentation

Lake.Reservoir

Package Registries #

This module contains definitions for fetching Lake package information from a online registry (e.g., Reservoir).

Package source information from a Lake registry (e.g., Reservoir). Only contains the subset of fields useful to Lake.

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

Package metadata from a Lake registry (e.g., Reservoir). Only contains the subset of fields useful to Lake.

Instances For
Equations
Equations
Equations
  • src.toJson = src.data
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Lake.uriEscapeByte (b : UInt8) (s : String := "") :

Encode a byte as a URI escape code (e.g., %20).

Equations
@[specialize #[]]
def Lake.foldlUtf8M {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (c : Char) (f : σUInt8m σ) (init : σ) :
m σ

Folds a monadic function over the UTF-8 bytes of Char from most significant to least significant.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev Lake.foldlUtf8 {σ : Type u_1} (c : Char) (f : σUInt8σ) (init : σ) :
σ
Equations
def Lake.uriEscapeChar (c : Char) (s : String := "") :

Encode a character as a sequence of URI escape codes representing its UTF8 encoding.

Equations
def Lake.uriEncodeChar (c : Char) (s : String := "") :

Encodes anything but a URI unreserved character as a URI escape sequences.

Equations

Encodes a string as an ASCII URI component, escaping special characters (and unicode).

Equations
def Lake.getUrl (url : String) (headers : Array String := #[]) :

Perform a HTTP GET request of a URL (using curl) and return the body.

Equations
  • One or more equations did not get rendered due to their size.
inductive Lake.ReservoirResp (α : Type u) :

A Reservoir API response object.

Instances For
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Lake.instFromJsonReservoirResp = { fromJson? := Lake.ReservoirResp.fromJson? }
def Lake.Reservoir.pkgApiUrl (lakeEnv : Lake.Env) (owner pkg : String) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.