297def modelWord32ModuloUnchecked =
298 (lambda unrestricted value : (family ModelWord32) .
299 (lambda unrestricted divisor : Nat .
300 (eliminate
301 ModelWord32
302 (lambda unrestricted current : (family ModelWord32) . Nat)
303 value
304 (branch
305 ModelWord32Value
306 b0
307 b1
308 b2
309 b3
310 .
311 (modelWord32ModuloStep
312 (modelWord32ModuloStep
313 (modelWord32ModuloStep (modelWord32ModuloStep zero b3 divisor) b2 divisor)
314 b1
315 divisor)
316 b0
317 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.