inductive Lake.BuildKey : Type

• 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

The type of keys in the Lake build store.

instance Lake.instInhabitedBuildKey : Inhabited Lake.BuildKey

instance Lake.instReprBuildKey : Repr Lake.BuildKey

instance Lake.instDecidableEqBuildKey : DecidableEq Lake.BuildKey

instance Lake.instHashableBuildKey : Hashable Lake.BuildKey

def Lake.BuildKey.toString (self : Lake.BuildKey) : String

instance Lake.BuildKey.instToStringBuildKey : ToString Lake.BuildKey

def Lake.BuildKey.quickCmp (k : Lake.BuildKey) (k' : Lake.BuildKey) : Ordering

theorem Lake.BuildKey.eq_of_quickCmp {k : Lake.BuildKey} {k' : Lake.BuildKey} : Lake.BuildKey.quickCmp k k' = Ordering.eq → k = k'

instance Lake.BuildKey.instLawfulCmpEqBuildKeyQuickCmp : Lake.LawfulCmpEq Lake.BuildKey Lake.BuildKey.quickCmp