The type of keys in the Lake build store.
- moduleFacet: Lake.Name → Lake.Name → Lake.BuildKey
- packageFacet: Lake.Name → Lake.Name → Lake.BuildKey
- targetFacet: Lake.Name → Lake.Name → Lake.Name → Lake.BuildKey
- customTarget: Lake.Name → Lake.Name → Lake.BuildKey
Instances For
Equations
- Lake.instInhabitedBuildKey = { default := Lake.BuildKey.moduleFacet default default }
Equations
- Lake.instReprBuildKey = { reprPrec := Lake.reprBuildKey✝ }
Equations
- Lake.instHashableBuildKey = { hash := Lake.hashBuildKey✝ }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Like the default toString
, but without disambiguation markers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.BuildKey.toSimpleString.eraseHead Lean.Name.anonymous = Lean.Name.anonymous
- Lake.BuildKey.toSimpleString.eraseHead (Lean.Name.anonymous.str str) = Lean.Name.anonymous
- Lake.BuildKey.toSimpleString.eraseHead (Lean.Name.anonymous.num i) = Lean.Name.anonymous
- Lake.BuildKey.toSimpleString.eraseHead (p.str s) = (Lake.BuildKey.toSimpleString.eraseHead p).str s
- Lake.BuildKey.toSimpleString.eraseHead (p.num s) = (Lake.BuildKey.toSimpleString.eraseHead p).num s
Instances For
Equations
- Lake.BuildKey.instToString = { toString := fun (x : Lake.BuildKey) => x.toString }
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Lake.BuildKey.eq_of_quickCmp
{k : Lake.BuildKey}
{k' : Lake.BuildKey}
:
k.quickCmp k' = Ordering.eq → k = k'