Equations
- Lake.instToTextModule = { toText := fun (x : Lake.Module) => x.name.toString }
Equations
- Lake.instToJsonModule = { toJson := fun (x : Lake.Module) => Lean.toJson x.name }
Equations
- Lake.instHashableModule = { hash := fun (m : Lake.Module) => hash m.keyName }
Equations
- Lake.instBEqModule = { beq := fun (m n : Lake.Module) => m.keyName == n.keyName }
@[reducible, inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[inline]
Instances For
@[reducible, inline]
Equations
Instances For
@[inline]
Equations
Instances For
Locate the named, buildable module in the library (which implies it is local and importable).
Equations
Instances For
Locate the named, buildable, importable, local module in the package.
Equations
Instances For
The library's buildable root modules.
Equations
- self.rootModules = Array.filterMap (fun (mod : Lean.Name) => Lake.LeanLib.findModule? mod self) self.config.roots
Instances For
@[inline]
Equations
Instances For
@[inline]
Instances For
@[inline]
Instances For
@[inline]
Equations
Instances For
@[inline]
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
Suffix for single module dynlibs (e.g., for precompilation).
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Instances For
@[inline]
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Instances For
@[inline]
Instances For
@[inline]
Instances For
@[inline]
Equations
Instances For
@[inline]
Instances For
@[inline]
Instances For
@[inline]
Instances For
@[inline]
Equations
Instances For
Trace Helpers #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.Module.instGetMTime = { getMTime := Lake.Module.getMTime }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.Module.instCheckExists = { checkExists := Lake.Module.checkExists }