Interface LeanPackage

interface LeanPackage {
lakeRoot: string;
lib: string;
name: string;
paperDir: string;
}

Properties

lakeRoot: string

Path to the paper's Lake package root, relative to repo root.

lib: string

Default [[lean_lib]] name (module root, e.g. "MyPaper").

name: string

Short-form package name used in lean.ref URI prefixes.

paperDir: string

Paper directory under folio/ (where the .ts/.md siblings live).