1379def stdU32DivRem =
1380 (lambda unrestricted dividend : (family ModelWord32) .
1381 (lambda unrestricted divisor : (family ModelWord32) .
1382 (nat-eliminate
1383 (lambda unrestricted current : Nat . (family StdDivision (family ModelWord32)))
1384 (constructor
1385 StdDivision
1386 StdDivisionFailed
1387 (family ModelWord32)
1388 (constructor StdDivisionErrorCode StdDivisionByZero))
1389 (lambda unrestricted predecessor : Nat .
1390 (lambda unrestricted induction : (family StdDivision (family ModelWord32)) .
1391 (eliminate
1392 StdU32DivisionState
1393 (lambda unrestricted current : (family StdU32DivisionState) .
1394 (family StdDivision (family ModelWord32)))
1395 (stdU32DivisionRun dividend divisor)
1396 (branch
1397 StdU32DivisionStateOf
1398 remainder
1399 quotient
1400 rest
1401 .
1402 (constructor
1403 StdDivision
1404 StdDivisionSucceeded
1405 (family ModelWord32)
1406 quotient
1407 remainder)))))
1408 (stdFlagNot (stdU32IsZero 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.