Lake.Build.Key

source

inductive Lake.BuildKey :

Type

The type of keys in the Lake build store.

moduleFacet: Lean.Name → Lean.Name → Lake.BuildKey
packageFacet: Lean.Name → Lean.Name → Lake.BuildKey
targetFacet: Lean.Name → Lean.Name → Lean.Name → Lake.BuildKey
customTarget: Lean.Name → Lean.Name → Lake.BuildKey

Instances For

source

instance Lake.instInhabitedBuildKey :

Inhabited Lake.BuildKey

Equations

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

source

instance Lake.instReprBuildKey :

Repr Lake.BuildKey

Equations

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

source

instance Lake.instDecidableEqBuildKey :

DecidableEq Lake.BuildKey

Equations

Lake.instDecidableEqBuildKey = Lake.decEqBuildKey✝

source

instance Lake.instHashableBuildKey :

Hashable Lake.BuildKey

Equations

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

source

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

String

Equations

(Lake.BuildKey.moduleFacet a a_1).toString = toString "+" ++ toString a ++ toString ":" ++ toString a_1 ++ toString ""
(Lake.BuildKey.packageFacet a a_1).toString = toString "@" ++ toString a ++ toString ":" ++ toString a_1 ++ toString ""
(Lake.BuildKey.targetFacet a a_1 a_2).toString = toString "" ++ toString a ++ toString "/" ++ toString a_1 ++ toString ":" ++ toString a_2 ++ toString ""
(Lake.BuildKey.customTarget a a_1).toString = toString "" ++ toString a ++ toString "/" ++ toString a_1 ++ toString ""

Instances For

source

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.
(Lake.BuildKey.moduleFacet a a_1).toSimpleString = toString "" ++ toString a ++ toString ":" ++ toString a_1 ++ toString ""
(Lake.BuildKey.packageFacet a a_1).toSimpleString = toString "" ++ toString a ++ toString ":" ++ toString a_1 ++ toString ""
(Lake.BuildKey.customTarget a a_1).toSimpleString = toString "" ++ toString a ++ toString "/" ++ toString a_1 ++ toString ""

Instances For

source

def Lake.BuildKey.toSimpleString.eraseHead :

Lean.Name → Lean.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

Instances For

source

instance Lake.BuildKey.instToString :

ToString Lake.BuildKey

Equations

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

source

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

Ordering

Equations

One or more equations did not get rendered due to their size.
(Lake.BuildKey.moduleFacet a a_1).quickCmp (Lake.BuildKey.moduleFacet m' f') = match a.quickCmp m' with | Ordering.eq => a_1.quickCmp f' | ord => ord
(Lake.BuildKey.moduleFacet a a_1).quickCmp k' = Ordering.lt
(Lake.BuildKey.packageFacet a a_1).quickCmp (Lake.BuildKey.moduleFacet module facet) = Ordering.gt
(Lake.BuildKey.packageFacet a a_1).quickCmp (Lake.BuildKey.packageFacet p' f') = match a.quickCmp p' with | Ordering.eq => a_1.quickCmp f' | ord => ord
(Lake.BuildKey.packageFacet a a_1).quickCmp k' = Ordering.lt
(Lake.BuildKey.targetFacet a a_1 a_2).quickCmp (Lake.BuildKey.customTarget package target) = Ordering.lt
(Lake.BuildKey.targetFacet a a_1 a_2).quickCmp k' = Ordering.gt
(Lake.BuildKey.customTarget a a_1).quickCmp (Lake.BuildKey.customTarget p' t') = match a.quickCmp p' with | Ordering.eq => a_1.quickCmp t' | ord => ord
(Lake.BuildKey.customTarget a a_1).quickCmp k' = Ordering.gt

Instances For

source

theorem Lake.BuildKey.eq_of_quickCmp {k : Lake.BuildKey} {k' : Lake.BuildKey} :

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

source

instance Lake.BuildKey.instLawfulCmpEqQuickCmp :

Lake.LawfulCmpEq Lake.BuildKey Lake.BuildKey.quickCmp

Equations

Lake.BuildKey.instLawfulCmpEqQuickCmp = ⋯