486def modelWord64SubtractChecked =
487 (lambda unrestricted left : (family ModelWord64) .
488 (lambda unrestricted right : (family ModelWord64) .
489 (nat-eliminate
490 (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
491 (constructor
492 ModelWord64CheckedResult
493 ModelWord64CheckedSucceeded
494 (modelWord64Subtract left right))
495 (lambda unrestricted predecessor : Nat .
496 (lambda unrestricted induction : (family ModelWord64CheckedResult) .
497 (constructor
498 ModelWord64CheckedResult
499 ModelWord64CheckedFailed
500 (constructor ModelWord64ArithmeticErrorCode ModelWord64SubtractionUnderflow))))
501 (modelWord64LessThan left right))))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.