def PropertyKindCalculus.Examples.length : KindOfProperty

The broad rational kind-of-quantity of dimension length.

Equations

• PropertyKindCalculus.Examples.length = { id := "length", scale := PropertyKindCalculus.ScaleType.ratio }

def PropertyKindCalculus.Examples.width : KindOfProperty

A sub-kind of length, individuated by its examination principle.

Equations

• PropertyKindCalculus.Examples.width = { id := "width", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "caliper-perpendicular" }

def PropertyKindCalculus.Examples.height : KindOfProperty

Another sub-kind of length, with a different examination principle.

Equations

• PropertyKindCalculus.Examples.height = { id := "height", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "caliper-vertical" }

inductive PropertyKindCalculus.Examples.Edge : KindOfProperty → KindOfProperty → Prop

This application's system of quantities: the direct-parent edges.

• width_length : Edge width length
• height_length : Edge height length

def PropertyKindCalculus.Examples.pencil : Object

Equations

• PropertyKindCalculus.Examples.pencil = { id := "pencil-0001" }

def PropertyKindCalculus.Examples.pencilWidth : IndividualProperty

Equations

• PropertyKindCalculus.Examples.pencilWidth = { kind := PropertyKindCalculus.Examples.width, carrier := PropertyKindCalculus.Examples.pencil }