266def modelWord64LessThan =
267 (lambda unrestricted left : (family ModelWord64) .
268 (lambda unrestricted right : (family ModelWord64) .
269 (eliminate
270 ModelWord64
271 (lambda unrestricted current : (family ModelWord64) . Nat)
272 left
273 (branch
274 ModelWord64Value
275 l0
276 l1
277 l2
278 l3
279 l4
280 l5
281 l6
282 l7
283 .
284 (eliminate
285 ModelWord64
286 (lambda unrestricted current : (family ModelWord64) . Nat)
287 right
288 (branch
289 ModelWord64Value
290 r0
291 r1
292 r2
293 r3
294 r4
295 r5
296 r6
297 r7
298 .
299 (modelWord64OrderByte
300 l7
301 r7
302 (modelWord64OrderByte
303 l6
304 r6
305 (modelWord64OrderByte
306 l5
307 r5
308 (modelWord64OrderByte
309 l4
310 r4
311 (modelWord64OrderByte
312 l3
313 r3
314 (modelWord64OrderByte
315 l2
316 r2
317 (modelWord64OrderByte l1 r1 (modelWord64OrderByte l0 r0 zero))))))))))))))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.