Nadja Yang
9f1cb0f57c
Verifies that buildLakePackage works with nix-only deps (no lake-manifest.json). Builds a proof of the weak minimax inequality from Mathlib.Order.CompleteLattice.Basic using leanDeps = [ mathlib ].
9 lines
114 B
Nix
9 lines
114 B
Nix
{
|
|
lib,
|
|
callPackage,
|
|
}:
|
|
|
|
lib.recurseIntoAttrs {
|
|
weak-minimax = callPackage ./weak-minimax/package.nix { };
|
|
}
|