Documentation

Lake.Build.Key

inductive Lake.BuildKey :

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.

Instances For

instance Lake.instInhabitedBuildKey :

Inhabited Lake.BuildKey

Equations

Lake.instInhabitedBuildKey = { default := Lake.BuildKey.moduleFacet default default }

instance Lake.instReprBuildKey :

Repr Lake.BuildKey

Equations

Lake.instReprBuildKey = { reprPrec := Lake.reprBuildKey✝ }

instance Lake.instDecidableEqBuildKey :

DecidableEq Lake.BuildKey

Equations

Lake.instDecidableEqBuildKey = Lake.decEqBuildKey✝

instance Lake.instHashableBuildKey :

Hashable Lake.BuildKey

Equations

Lake.instHashableBuildKey = { hash := Lake.hashBuildKey✝ }

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

Equations

One or more equations did not get rendered due to their size.

Instances For

instance Lake.BuildKey.instToStringBuildKey :

ToString Lake.BuildKey

Equations

Lake.BuildKey.instToStringBuildKey = { toString := fun x => Lake.BuildKey.toString x }

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

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} :

Lake.BuildKey.quickCmp k k' = Ordering.eq → k = k'

instance Lake.BuildKey.instLawfulCmpEqBuildKeyQuickCmp :

Lake.LawfulCmpEq Lake.BuildKey Lake.BuildKey.quickCmp

Equations

Lake.BuildKey.instLawfulCmpEqBuildKeyQuickCmp = Lake.LawfulCmpEq.mk @Lake.BuildKey.instLawfulCmpEqBuildKeyQuickCmp.proof_1