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.
- git (data : JsonObject) (url : String) (githubUrl? defaultBranch? : Option String) (subDir? : Option System.FilePath) : RegistrySrc
- other (data : JsonObject) : RegistrySrc
Instances For
Equations
Instances For
Package metadata from a Lake registry (e.g., Reservoir). Only contains the subset of fields useful to Lake.
- name : String
- fullName : String
- sources : Array RegistrySrc
- data : Lean.Json
Instances For
Equations
Instances For
Encode a byte as a URI escape code (e.g., %20
).
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Encode a character as a sequence of URI escape codes representing its UTF8 encoding.
Equations
Instances For
Encodes anything but a URI unreserved character as a URI escape sequences.
Equations
Instances For
Encodes a string as an ASCII URI component, escaping special characters (and unicode).
Equations
Instances For
A Reservoir API response object.
- data {α : Type u} (a : α) : ReservoirResp α
- error {α : Type u} (status : Nat) (message : String) : ReservoirResp α