the exact value as a fraction
123def specFraction =
124 (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
125 (nat-eliminate (lambda unrestricted current : Nat . (family SpecFraction))
126 (constructor SpecFraction SpecFractionOf (nat-multiply digits (specPow10 exponent)) 1)
127 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecFraction) .
128 (constructor SpecFraction SpecFractionOf digits (specPow10 exponent))))
129 exponentNegative))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.