U64 division: divisor zero -> StdDivisionByZero, else quotient + remainder.
1266def stdU64DivRem =
1267 (lambda unrestricted dividend : (family ModelWord64) .
1268 (lambda unrestricted divisor : (family ModelWord64) .
1269 (nat-eliminate
1270 (lambda unrestricted current : Nat . (family StdDivision (family ModelWord64)))
1271 (constructor
1272 StdDivision
1273 StdDivisionFailed
1274 (family ModelWord64)
1275 (constructor StdDivisionErrorCode StdDivisionByZero))
1276 (lambda unrestricted predecessor : Nat .
1277 (lambda unrestricted induction : (family StdDivision (family ModelWord64)) .
1278 (eliminate
1279 StdU64DivisionState
1280 (lambda unrestricted current : (family StdU64DivisionState) .
1281 (family StdDivision (family ModelWord64)))
1282 (stdU64DivisionRun dividend divisor)
1283 (branch
1284 StdU64DivisionStateOf
1285 remainder
1286 quotient
1287 rest
1288 .
1289 (constructor
1290 StdDivision
1291 StdDivisionSucceeded
1292 (family ModelWord64)
1293 quotient
1294 remainder)))))
1295 (modelWord64FlagNot (modelWord64IsZero 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.