90noncomputable def equalityCost (K : Type*) (weight : ℝ) : K → K → ℝ :=
proof body
Definition body.
91 fun x y => if x = y then 0 else weight 92 93/-! ## The Three Definitional Facts 94 95The following three theorems show that an equality-induced cost 96automatically satisfies three of the four Aristotelian conditions 97without any structural assumption beyond the type signature. 98-/ 99 100/-- **(L1) Identity, derived.** The equality-induced cost satisfies 101`C(x, x) = 0` definitionally. This is not an axiom; it is the 102definitional content of "comparing a thing with itself takes no work," 103forced by reflexivity of equality. -/
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.