132def normalizationCostFromMagnitude =
133 (lambda unrestricted digits : Bytes .
134 (eliminate
135 NaturalMagnitudeResult
136 (lambda unrestricted current : (family NaturalMagnitudeResult) .
137 (family NormalizationCostResult))
138 (Compiler.NaturalMagnitude/magnitudeDecodeCanonical digits)
139 (branch
140 NaturalMagnitudeAccepted
141 canonical
142 .
143 (app
144 (nat-eliminate
145 (lambda unrestricted tooLong : Nat .
146 (pi unrestricted force : Nat . (family NormalizationCostResult)))
147 (lambda unrestricted force : Nat .
148 (app
149 (nat-eliminate
150 (lambda unrestricted empty : Nat .
151 (pi unrestricted force : Nat . (family NormalizationCostResult)))
152 (lambda unrestricted force : Nat .
153 (finishNormalizationCostWord
154 (Compiler.IntegerLiteral/integerLiteralParse
155 (constructor IntegerLiteralRadix IntegerLiteralDecimal)
156 (constructor IntegerLiteralKind IntegerLiteralUnsigned)
157 (constructor IntegerLiteralSign IntegerLiteralPositive)
158 (constructor IntegerLiteralWidth IntegerLiteralWidth32)
159 (normalizationCostDecimalText canonical))))
160 (lambda unrestricted predecessor : Nat .
161 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationCostResult)) .
162 (lambda unrestricted force : Nat .
163 (constructor
164 NormalizationCostResult
165 NormalizationCostWord
166 Model.Word32/modelWord32Zero))))
167 (bytes-equal canonical b""))
168 zero))
169 (lambda unrestricted predecessor : Nat .
170 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NormalizationCostResult)) .
171 (lambda unrestricted force : Nat .
172 (constructor NormalizationCostResult NormalizationCostTooLarge))))
173 (nat-less-than (byte-to-nat (byte 10)) (bytes-length canonical)))
174 zero))
175 (branch
176 NaturalMagnitudeRejected
177 failure
178 .
179 (constructor NormalizationCostResult NormalizationCostInvalid))))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.