184def magnitudeParseDigits =
185 (lambda unrestricted radix : (family IntegerLiteralRadix) .
186 (lambda unrestricted digits : Bytes .
187 (app
188 (nat-eliminate
189 (lambda unrestricted flag : Nat .
190 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
191 (lambda unrestricted force : Nat .
192 (eliminate
193 IntegerLiteralSyntaxResult
194 (lambda unrestricted current : (family IntegerLiteralSyntaxResult) .
195 (family NaturalMagnitudeResult))
196 (Compiler.IntegerLiteral/integerLiteralValidateSeparators radix digits)
197 (branch
198 IntegerLiteralSyntaxAccepted
199 .
200 (magnitudeConvertValidatedDigits
201 radix
202 (Compiler.IntegerLiteral/integerLiteralStripSeparators digits)))
203 (branch
204 IntegerLiteralSyntaxFailed
205 failure
206 .
207 (constructor
208 NaturalMagnitudeResult
209 NaturalMagnitudeRejected
210 (constructor NaturalMagnitudeFailure NaturalMagnitudeLiteralMalformed failure)))))
211 (lambda unrestricted predecessor : Nat .
212 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
213 (lambda unrestricted force : Nat .
214 (constructor
215 NaturalMagnitudeResult
216 NaturalMagnitudeRejected
217 (constructor
218 NaturalMagnitudeFailure
219 NaturalMagnitudeLiteralMalformed
220 (constructor IntegerLiteralFailure IntegerLiteralMissingDigits))))))
221 (bytes-equal digits b""))
222 zero)))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.