the exact value as a fraction
126def specFraction =
127 (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
128 (nat-eliminate (lambda unrestricted current : Nat . (family SpecFraction))
129 (constructor SpecFraction SpecFractionOf (nat-multiply digits (specPow10 exponent)) 1)
130 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecFraction) .
131 (constructor SpecFraction SpecFractionOf digits (specPow10 exponent))))
132 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.