inductive Lake.BuildKey : Type

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

• Lake.BuildKey.instLawfulCmpEqQuickCmp
• Lake.BuildKey.instToString
• Lake.instHashableBuildKey
• Lake.instInhabitedBuildKey
• Lake.instMonadCycleOfBuildKeyRecBuildM
• Lake.instReprBuildKey

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) : String

Equations

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

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

Like the default toString, but without disambiguation markers.

Equations

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

def Lake.BuildKey.toSimpleString.eraseHead : Lake.Name → Lake.Name

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

instance Lake.BuildKey.instToString : ToString Lake.BuildKey

Equations

• Lake.BuildKey.instToString = { toString := fun (x : Lake.BuildKey) => x.toString }

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

Equations

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

Instances For

• Lake.BuildKey.instLawfulCmpEqQuickCmp

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

instance Lake.BuildKey.instLawfulCmpEqQuickCmp : Lake.LawfulCmpEq Lake.BuildKey Lake.BuildKey.quickCmp

Equations

• Lake.BuildKey.instLawfulCmpEqQuickCmp = Lake.LawfulCmpEq.mk @Lake.BuildKey.instLawfulCmpEqQuickCmp.proof_1