319def modelWord32Modulo =
320 (lambda unrestricted value : (family ModelWord32) .
321 (lambda unrestricted divisor : Nat .
322 (nat-eliminate
323 (lambda unrestricted current : Nat . (family ModelWord32ModuloResult))
324 (constructor
325 ModelWord32ModuloResult
326 ModelWord32ModuloFailed
327 (constructor ModelWord32ArithmeticErrorCode ModelWord32ModuloByZero))
328 (lambda unrestricted predecessor : Nat .
329 (lambda unrestricted induction : (family ModelWord32ModuloResult) .
330 (constructor
331 ModelWord32ModuloResult
332 ModelWord32ModuloSucceeded
333 (modelWord32ModuloUnchecked value divisor))))
334 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.