Unit declarations, and why conflicting ones are rejected

dimension Velocity = Length/Time is an abbreviation: dimensions are exponent vectors, so it expands, and its only check is scoping (DimAbbrev.elabDimDefs). Unit declarations are the interesting case, because

unit yard = 3 foot

declares a generator and an equation, and equations can conflict: with units nameable in terms of other units, two routes from yard to meter need not agree, and nothing in the algebra of units (a free ℚ-vector space) forces them to. LambdaS.Conversion contrasts this with a design that sidesteps route ambiguity by allowing at most one named unit per dimension.

What the resolution is, and what it is not

It is not a consistency check on paths. A valuation (a Scaling B 0) assigns each base unit a positive real magnitude, and LambdaS.Conversion already makes conversion a ratio of one valuation, so convChain_eq says any chain of intermediate conversions equals the direct factor: path independence is a theorem there, not an obligation here.

What is left is the prior question: do the declarations determine a valuation at all? That is a linear system, and this file gives its solvability criterion, in both directions. dependency_forces is necessity: under a satisfying valuation, every ℚ-linear combination of the declared ratios whose unit exponents cancel forces the same combination of log-factors to vanish (dependency_forces_mul says the factors multiply to one). dependency_sufficient is sufficiency: respect every dependency and a satisfying valuation exists, so consistent_iff_dependencies characterizes consistency outright. Its multiplicative form, consistent_iff_dependencies_mul, is Theorem 3.1 of our paper. factor_chain is the two-step instance that is literally the yard/foot/meter conflict. not_satisfiable_of_chain turns it around: get the arithmetic wrong and no valuation exists, so the declaration set is rejected rather than silently picking a route.

Where exactness lives

The criterion is exact rational arithmetic even though valuations are real. Declared factors are rationals; a dependency demands ∏ qᵢ^{cᵢ} = 1 with cᵢ rational, which clearing denominators turns into an identity in ℚ. Rational powers can require irrational magnitudes: if V(c) = 2, then V(c^(1/2)) = √2. Valuations therefore range over ℝ. The checker (DeclSolver.solve, eliminating over LogFactor) manipulates symbolic logarithmic expressions exactly; it evaluates no logarithms or roots. Declarations live in ℚ⁺, and the consistency tests reduce to equality in ℚ⁺.

What is not declared has no factor

A base unit with no declaration is a primitive, and its magnitude is free. So meter and foot as bare generators are same-dimension units with no determined conversion factor: convert between them typechecks, but its value is whatever the valuation says. Declaring unit foot = 0.3048 meter is exactly what pins it. DeclSolver.check in LambdaS.DeclareSolver enforces the execution obligation: declarations must be dimensionally sound, consistent, and determine every same-dimension factor. DeclSolver.conversionExact supports individual lookup. For a consistent set it returns an exact radical when the ratio is determined and none when it is not; it does not silently supply an arbitrary missing factor. The semantic criterion below is linked to those executable checks by soundness and completeness proofs (DeclSolver.solve_isSome_iff, DeclSolver.check_isSome_iff).

Unit Declarations

The worked examples this section cites by bare name, such as yard_satisfiable, cycle_conflict, and dimCycle, are in LambdaS.Examples.

Conversion forces a question the parametric literature never faces: where do the factors come from? The answer is unit declarations, in the style scientists write them:

unit yard = 3 foot;  unit foot = 0.3048 meter.

Declarations are not terms of Λs: they are the interface a surface language hands to the calculus, and the artifact consumes them as data (as Decl values). Each declaration constrains one unit against another by a factor; in unit yard = 3 foot, the declared factor is 3.

Declarations can conflict. With units nameable in terms of other units, a system that implements conversion by walking the declared structure can offer more than one route between two units, with no guarantee the routes agree: add the redundant declaration yard = 0.9 meter and the direct route disagrees with the route through feet, since 3 × 0.3048 = 0.9144 ≠ 0.9 (see note 1). Choosing a route through declared factors without checking consistency can cause this defect, and nothing in the algebra of units forbids it: the units form a free ℚ-vector space (“Units and Dimensions” (Typing.lean)), and the declared factors are data the algebra does not constrain.

Note 1. Redundant declarations are not a strawman: real unit databases can carry them deliberately, because lookup through a hub unit loses precision that a directly stored factor preserves. The design question is not whether redundancy occurs but what happens when it disagrees.

Dimension declarations, by contrast, carry no factor, and the only check they need is scoping. A bare one, dimension Length, introduces a base dimension; freshness is its whole check, and the bare declarations jointly supply the calculus's parameter D. One with a right-hand side is an abbreviation: it introduces a fresh name for a vector over the base dimensions, its right-hand side mentioning only base dimensions and earlier abbreviations, and expands at once: dimension Velocity = Length/Time is the vector (Length ↦ 1, Time ↦ -1) from then on. Cycles are consequently not detected but unrepresentable: the incorrect pair Velocity = Length/Time, Length = Velocity/Time is rejected at its second line for rebinding a generator, before any question of consistency can arise, and a forward reference is rejected because an undefined name does not denote (DimAbbrev.elabDimDefs; the cyclic pair is dimCycle). Base units are declared the same way, by a dimension and no factor: unit meter : Length makes meter primary (the term is from [Allen et al. 2004]; the syntax is Fortress's [Allen et al. 2006]), and the declaration is what determines the unit's dimension. The primary declarations jointly supply the calculus's parameters B and dim, and they too need only scoping (DimAbbrev.elabPrimary): a fresh name, and a dimension that denotes. This section is therefore about the declarations that carry a factor.

Λs does not implement conversion as a walk. A valuation V (a Scaling B 0 in the artifact) assigns each base unit a positive magnitude: an exchange-rate table into an arbitrary fixed reference scale, not a measurement. For example, V(meter) = 1, V(foot) = 0.3048, V(yard) = 0.9144 is a valuation, and it satisfies both declarations above. A valuation extends to a homomorphism from unit expressions to (ℝ^(>0),×), and the conversion factor from u to v is the ratio conv_V(u,v) = V(u)/V(v). Path independence is then a theorem rather than a proof obligation (any chain of intermediate conversions telescopes to the direct factor). Declarations constrain valuations; we say a declaration set is consistent when some valuation satisfies every declared equation. Note that declarations carry no order, and no acyclicity condition is imposed or needed: each declaration is an equation, the set is a simultaneous system, and a cycle is just a dependency the criterion below decides. The benign cycle yard = 3 foot, foot = 1/3 yard is satisfiable (cycle_satisfiable); close it wrongly, with foot = yard, and the dependency forces 3 = 1, so no valuation exists (cycle_conflict). Nor can a declaration mention an undeclared generator: the base units are the calculus's parameter B, so the reference is unrepresentable. What remains is the prior question: do the declarations determine a valuation at all?

A declaration unit b = q w constrains the ratio b/w to the value q ∈ ℚ^(>0). In logarithmic coordinates each declaration is one linear equation in the unknowns log V(b), so a valuation exists exactly when that linear system is consistent: every linear dependency among the constrained ratios must force the matching relation among the declared factors. Both directions are theorems. Necessity holds (dependency_forces; in product form, dependency_forces_mul). Sufficiency invites a worry. The unknowns log V(b) are real, and necessarily so: valuations are real-valued, not merely their logarithms, since rational exponents can force irrational magnitudes (declare c = 2 and b = c^(1/2), and every satisfying valuation has V(b) = √2), and rational magnitudes can have irrational logarithms (though log 1 = 0). The dependencies, by contrast, are rational, so we might fear a real-coefficient dependency imposing a constraint the rational ones miss. None does: ℝ is itself a vector space over ℚ, its vectors the reals and its scalars the rationals, so the rational coefficient matrix has the same dependencies over either field, and the system is solved ℚ-linearly with real values (dependency_sufficient).

Theorem 3.1 (Consistency; consistent_iff_dependencies_mul). A finite declaration set with ratios r_i and positive rational factors q_i admits a satisfying valuation if and only if, for every ℚ-linear combination with ∑_i c_i r_i = 0 in the unit group, ∏_i q_i^c_i = 1; equivalently, in logarithmic form, ∑_i c_i log q_i = 0 (consistent_iff_dependencies).

With the criterion in hand, we work the example in full. The three declarations

unit yard = 3 foot;  unit foot = 0.3048 meter;  unit yard = 0.9144 meter

constrain the ratios r₁ = yard/foot, r₂ = foot/meter, and r₃ = yard/meter. Writing y, f, m for log V(yard), log V(foot), log V(meter), they induce the linear system

y - f = log 3,  f - m = log 0.3048,  y - m = log 0.9144.

The ratios are linearly dependent: with coefficients c = (1, 1, -1) in Theorem 3.1 (consistent_iff_dependencies_mul), r₁ + r₂ - r₃ = 0 in the unit group (multiplicatively, (yard/foot)(foot/meter)(meter/yard) is the dimensionless 1), so consistency demands q₁ q₂ q₃⁻¹ = 1, that is, 3 × 0.3048 = 0.9144 (see note 2). The equation holds, and the artifact exhibits a satisfying valuation explicitly (yard_satisfiable): the exchange-rate table V above. Now replace the third declaration by yard = 0.9 meter. The same dependency demands 3 × 0.3048 = 0.9, which is false; the artifact refutes the set (yard_conflict): no valuation satisfies all three, the set is rejected at declaration time, and there is never a choice of route to get wrong. Because coefficients and factors are rational, the test uses exact arithmetic. Symbolic logarithmic expressions are manipulated without numerical evaluation; denominator clearing reduces their zero tests to rational product equality. Note that a satisfied redundant declaration has no freedom in its factor: any valuation satisfying all three declarations forces 3 × 0.3048 = 0.9144 (yard_forced), and the general lemma (factor_chain_consistent) states this for an arbitrary third declaration.

Note 2. The yard has been exactly 0.9144 meters only since 1959, when the United States and five other English-speaking countries adopted a common yard, the American one moving by two parts per million [Astin and Karo 1959]. The United States kept its earlier foot for surveying; that redundant declaration, inconsistent with the new one in the seventh decimal place, survived until its retirement, effective December 31, 2022, announced by a 2020 Federal Register notice [NIST and NOAA 2020].

Note that a base unit with no declaration is a primitive, and its magnitude is free. Its dimension is not: the unit system assigns every base unit a dimension (dim : B → ℚ^D is total, “Units and Dimensions” (Typing.lean)), so declarations add magnitudes, never dimensions. Declarations, not the type system, give conversion its numeric content; the type system contributes a separate, decidable check that each declaration relates units of one dimension: unit yard = 3 second fails Decl.Sound, and DeclSolver.check rejects it. That check is orthogonal to Theorem 3.1 (consistent_iff_dependencies_mul).

What the declared numbers are worth to running code is the subject of Section 7 of our paper (Adequacy and Erasure), where Theorem 7.1 (evalC_convert_declared, in LambdaS.Adequacy) closes the chain from declaration to real-valued evaluation: the evaluator instantiated with real arithmetic converts one yard into feet by multiplying by the declared 3 and into meters by the forced 0.9144 (one_yard_is_three_feet; through the forced factor, one_yard_in_meters).

Declarations

structure LambdaS.Decl (B : Type) : Type

A unit declaration: unit lhs = factor · rhs.

The factor is a positive rational. That is not a convenience; it is what keeps the consistency criterion exact, since a product of rational powers of rationals is decidably one.

• lhs : B

  The unit being declared, a base unit. The declaration constrains its magnitude; it does not define the unit away in terms of rhs.

• factor : ℚ

  The declared magnitude, against rhs.

• pos : 0 < self.factor

  Positivity. A unit of negative magnitude is not a unit.

• rhs : UExp B 0

  What it is declared against: any unit expression, compound or not.

def LambdaS.Decl.ratio {B : Type} [DecidableEq B] (d : Decl B) : UExp B 0

The ratio a declaration constrains: lhs / rhs, which the declaration says has magnitude factor. Dimensionless when the declaration is sound.

Equations

• d.ratio = (LambdaS.Term.ofBase d.lhs).div d.rhs

def LambdaS.Decl.Satisfies {B : Type} [Fintype B] [DecidableEq B] (ψ : Scaling B 0) (d : Decl B) : Prop

A valuation satisfies a declaration when it assigns the declared magnitude to the declared ratio.

Equations

• LambdaS.Decl.Satisfies ψ d = (ψ.scale d.ratio = ↑d.factor)

theorem LambdaS.Decl.satisfies_iff {B : Type} [Fintype B] [DecidableEq B] {ψ : Scaling B 0} {d : Decl B} : Satisfies ψ d ↔ ψ.scale (Term.ofBase d.lhs) = ↑d.factor * ψ.scale d.rhs

The multiplicative reading, which is how a declaration is written.

theorem LambdaS.Decl.satisfies_iff_log {B : Type} [Fintype B] [DecidableEq B] {ψ : Scaling B 0} {d : Decl B} : Satisfies ψ d ↔ ψ.logScale d.ratio = Real.log ↑d.factor

The additive reading, in log coordinates. This is the form the linear algebra runs on: a declaration is one linear equation in the unknowns ψ.base.

theorem LambdaS.Decl.conv_eq_factor {B : Type} [Fintype B] [DecidableEq B] {ψ : Scaling B 0} {d : Decl B} (h : Satisfies ψ d) : conv ψ (Term.ofBase d.lhs) d.rhs = ↑d.factor

A declaration determines its conversion factor. Whatever valuation satisfies it, converting the declared unit into its right-hand side gives exactly the declared number.

This is the link between declarations and LambdaS.Conversion: the declared factor is the conversion factor, so path independence transfers wholesale.

Dimensional soundness

def LambdaS.Decl.Sound {B D : Type} [Fintype B] [UnitSys B D] (d : Decl B) : Prop

A declaration is sound when the declared unit has the dimension of its right-hand side. Decidable, and it is what stops a declaration smuggling in a conversion between dimensions: unit yard = 3 second is not sound, and DeclSolver.check rejects any declaration set containing it.

Equations

• d.Sound = (LambdaS.UnitSys.dim d.lhs = LambdaS.dimOf (LambdaS.DCtx.nil D) d.rhs)

@[instance_reducible]

instance LambdaS.Decl.instDecidableSoundOfFintypeOfDecidableEq {B D : Type} [Fintype B] [UnitSys B D] [Fintype D] [DecidableEq D] (d : Decl B) : Decidable d.Sound

Equations

• d.instDecidableSoundOfFintypeOfDecidableEq = id inferInstance

theorem LambdaS.Decl.dimOf_ofBase {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] (b : B) : dimOf (DCtx.nil D) (Term.ofBase b) = UnitSys.dim b

The dimension of a bare generator is its declared dimension.

theorem LambdaS.Decl.sameDim_of_sound {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {d : Decl B} (h : d.Sound) : SameDim (DCtx.nil D) (Term.ofBase d.lhs) d.rhs

Sound declarations declare interchangeable units. So the declared unit and its right-hand side pass the convert check, and the declaration is usable.

theorem LambdaS.Decl.ratio_dimensionless {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {d : Decl B} (h : d.Sound) : dimOf (DCtx.nil D) d.ratio = 1

A sound declaration has a dimensionless ratio. Which is why the factor is a pure number, and why it can itself be named as a unit.

Consistency

A declaration set is a linear system in log coordinates. It is solvable exactly when the factors respect every dependency among the unit parts, and that is the criterion for the declarations to have a satisfying valuation. Uniqueness of conversion factors is the separate determinacy question in LambdaS.Determinacy.

theorem LambdaS.dependency_forces {B : Type} [Fintype B] [DecidableEq B] {ψ : Scaling B 0} {n : ℕ} {ds : Fin n → Decl B} (h : ∀ (i : Fin n), Decl.Satisfies ψ (ds i)) (c : Fin n → ℚ) (hcancel : ∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = 0) : ∑ i : Fin n, ↑(c i) * Real.log ↑(ds i).factor = 0

The general criterion. Any ℚ-linear combination of the declared ratios that cancels in the unit group forces the same combination of log-factors to vanish.

Contrapositively: exhibit a dependency whose factors do not multiply to one, and no valuation exists; the declaration set is rejected. Since the coefficients are rational and the factors are rational, that test is exact arithmetic.

theorem LambdaS.dependency_forces_mul {B : Type} [Fintype B] [DecidableEq B] {ψ : Scaling B 0} {n : ℕ} {ds : Fin n → Decl B} (h : ∀ (i : Fin n), Decl.Satisfies ψ (ds i)) (c : Fin n → ℚ) (hcancel : ∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = 0) : ∏ i : Fin n, ↑(ds i).factor ^ ↑(c i) = 1

The multiplicative form of dependency_forces: the same rational combination of declared factors, read as a product of real powers, equals 1. The two forms are equivalent because every factor is positive, so Real.log and Real.exp translate between the product and the sum.

Sufficiency

The converse direction. dependency_forces says a satisfying valuation makes every dependency respect the factors; here we show that respecting the dependencies is all it takes, so the criterion decides consistency outright.

The proof needs no linear algebra over ℝ. The system asks for a function B → ℝ in log coordinates, and ℝ is a vector space over ℚ, so the system can be solved ℚ-linearly with values in ℝ: send each ratio's exponent vector to its log-factor, check the assignment kills every rational dependency (the hypothesis), factor it through the span of the exponent vectors, and extend to all of B → ℚ. The question of whether real dependencies among rational vectors exceed the rational ones never arises.

theorem LambdaS.dependency_sufficient {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} {ds : Fin n → Decl B} (h : ∀ (c : Fin n → ℚ), (∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = 0) → ∑ i : Fin n, ↑(c i) * Real.log ↑(ds i).factor = 0) : ∃ (ψ : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies ψ (ds i)

The criterion is sufficient. If every ℚ-linear dependency among the declared ratios forces the matching combination of log-factors to vanish, then some valuation satisfies every declaration at once.

This is the converse of dependency_forces and the sufficiency half of Theorem 3.1 (Consistency) in our paper. In log coordinates each declaration is one linear equation in the unknown base magnitudes; the hypothesis is exactly that the right-hand sides respect the dependencies of the left-hand sides, and exists_linearMap_of_dependencies turns that into a ℚ-linear map on B → ℚ with values in ℝ. Reading that map on the standard basis gives the valuation.

theorem LambdaS.consistent_iff_dependencies {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} {ds : Fin n → Decl B} : (∃ (ψ : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies ψ (ds i)) ↔ ∀ (c : Fin n → ℚ), (∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = 0) → ∑ i : Fin n, ↑(c i) * Real.log ↑(ds i).factor = 0

Consistency, characterized. A declaration set has a satisfying valuation exactly when every ℚ-linear dependency among its ratios forces the matching combination of log-factors to vanish. Necessity is dependency_forces; sufficiency is dependency_sufficient. This is the solvability criterion in the form the linear algebra produces it.

theorem LambdaS.consistent_iff_dependencies_mul {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} {ds : Fin n → Decl B} : (∃ (ψ : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies ψ (ds i)) ↔ ∀ (c : Fin n → ℚ), (∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = 0) → ∏ i : Fin n, ↑(ds i).factor ^ ↑(c i) = 1

Consistency, in the multiplicative form of Theorem 3.1 in our paper. A declaration set has a satisfying valuation exactly when every ℚ-linear dependency among its ratios forces the corresponding product of declared factors to one. Since the coefficients and factors are rational, the right-hand side is an exact arithmetic test.

The conflict, exhibited

Three declarations, two routes from the first unit to the last. This is the running example of Section 3 of our paper: yard = 3 foot, foot = 0.3048 meter, and a redundant yard = q meter. LambdaS.Examples instantiates these lemmas (yard_forced, yard_conflict).

theorem LambdaS.factor_chain {B : Type} [Fintype B] [DecidableEq B] {ψ : Scaling B 0} {a b c : Decl B} (ha : Decl.Satisfies ψ a) (hb : Decl.Satisfies ψ b) (hc : Decl.Satisfies ψ c) (h1 : a.rhs = Term.ofBase b.lhs) (h2 : a.lhs = c.lhs) (h3 : b.rhs = c.rhs) : ↑(a.factor * b.factor) = ↑c.factor

Chained declarations force the factor. If a is declared against b's unit, b against some w, and c declares a's unit directly against the same w, then any valuation satisfying all three forces a.factor * b.factor = c.factor.

There is no freedom here and no route to choose. The redundant declaration is either arithmetically correct or the system has no solution.

theorem LambdaS.not_satisfiable_of_chain {B : Type} [Fintype B] [DecidableEq B] {a b c : Decl B} (h1 : a.rhs = Term.ofBase b.lhs) (h2 : a.lhs = c.lhs) (h3 : b.rhs = c.rhs) (hbad : a.factor * b.factor ≠ c.factor) : ¬∃ (ψ : Scaling B 0), Decl.Satisfies ψ a ∧ Decl.Satisfies ψ b ∧ Decl.Satisfies ψ c

Conflicting declarations are rejected. Get the arithmetic wrong and no valuation satisfies all three, so there is nothing for an implementation to pick between: DeclSolver.solve rejects any declaration set containing them (DeclSolver.solve_isSome_iff).

A converter that walks declared factors must choose a route and can choose wrongly; here the situation that would force a choice is precisely the situation with no solution.

theorem LambdaS.factor_chain_consistent {B : Type} [Fintype B] [DecidableEq B] {ψ : Scaling B 0} {a b c : Decl B} (ha : Decl.Satisfies ψ a) (hb : Decl.Satisfies ψ b) (hc : Decl.Satisfies ψ c) (h1 : a.rhs = Term.ofBase b.lhs) (h2 : a.lhs = c.lhs) (h3 : b.rhs = c.rhs) : a.factor * b.factor = c.factor

Joint satisfaction forces consistency: factor_chain with the cast removed, stated in ℚ for symmetry with not_satisfiable_of_chain: if one valuation satisfies all three declarations, their factors obey the chain equation exactly.

Dimension abbreviations

Unit declarations constrain; dimension declarations abbreviate. A dimension declaration introduces a fresh name for a vector over the base dimensions, so the only check it needs is scoping: the name must be new, and the right-hand side may mention only base dimensions and earlier abbreviations. Under that discipline a cyclic pair such as Velocity = Length/Time; Length = Velocity/Time is rejected at its second line, for rebinding a generator, before any question of consistency can arise; a forward reference is rejected because an undefined name does not denote. Cycles are not detected but unrepresentable.

@[reducible, inline]

abbrev LambdaS.DimAbbrev.Ref (D : Type) : Type

One right-hand-side factor: a base dimension or an earlier abbreviation, at a rational exponent.

Equations

• LambdaS.DimAbbrev.Ref D = ((D ⊕ String) × ℚ)

def LambdaS.DimAbbrev.elabOne {D : Type} [DecidableEq D] (baseName : String → Option D) (env : List (String × DExp D 0)) (n : String) (rhs : List (Ref D)) : Option (List (String × DExp D 0))

Elaborate one abbreviation against the environment built so far. Rejects a name that collides with a base dimension or an earlier abbreviation, and a reference to a name not yet defined.

Equations

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

def LambdaS.DimAbbrev.elabDimDefs {D : Type} [DecidableEq D] (baseName : String → Option D) : List (String × List (Ref D)) → Option (List (String × DExp D 0))

Elaborate a sequence of dimension abbreviations, in order. Every name that survives maps to an exponent vector over the base dimensions; nothing else survives.

Equations

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

def LambdaS.DimAbbrev.elabPrimary {D : Type} [DecidableEq D] (baseName : String → Option D) (dims : List (String × DExp D 0)) : List (String × (D ⊕ String)) → Option (List (String × DExp D 0))

Primary-unit declarations. A base unit is introduced by naming it and its dimension, with no factor: unit meter : Length makes meter primary (the term is from Allen et al. 2004; the syntax is Fortress's), and the declaration is what determines the unit's dimension. Elaboration is scoping again: a fresh unit name, and a dimension that denotes (a base dimension or an abbreviation already elaborated). The surviving table is the calculus's parameter UnitSys.dim on the declared generators, which dimOf extends to unit expressions (Decl.dimOf_ofBase).

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.DimAbbrev.elabPrimary baseName dims [] = some []