Validate both operands before invoking a checked binary operation.
340def magnitudeBinaryChecked =
341 (lambda unrestricted operation : (pi unrestricted left : Bytes . (pi unrestricted right : Bytes . (family NaturalMagnitudeResult))) .
342 (lambda unrestricted left : Bytes .
343 (lambda unrestricted right : Bytes .
344 (eliminate
345 NaturalMagnitudeResult
346 (lambda unrestricted current : (family NaturalMagnitudeResult) .
347 (family NaturalMagnitudeResult))
348 (magnitudeDecodeCanonical left)
349 (branch
350 NaturalMagnitudeAccepted
351 a
352 .
353 (eliminate
354 NaturalMagnitudeResult
355 (lambda unrestricted current : (family NaturalMagnitudeResult) .
356 (family NaturalMagnitudeResult))
357 (magnitudeDecodeCanonical right)
358 (branch NaturalMagnitudeAccepted b . (operation a b))
359 (branch
360 NaturalMagnitudeRejected
361 error
362 .
363 (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))
364 (branch
365 NaturalMagnitudeRejected
366 error
367 .
368 (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))))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.