401def modelWord32Modulo =
402 (lambda unrestricted value : (family ModelWord32) .
403 (lambda unrestricted divisor : Nat .
404 (nat-eliminate
405 (lambda unrestricted current : Nat . (family ModelWord32ModuloResult))
406 (constructor
407 ModelWord32ModuloResult
408 ModelWord32ModuloFailed
409 (constructor ModelWord32ArithmeticErrorCode ModelWord32ModuloByZero))
410 (lambda unrestricted predecessor : Nat .
411 (lambda unrestricted induction : (family ModelWord32ModuloResult) .
412 (constructor
413 ModelWord32ModuloResult
414 ModelWord32ModuloSucceeded
415 (modelWord32ModuloUnchecked value divisor))))
416 divisor)))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.