Order one byte position: 1 when left is below right, 0 when above, and the
lower positions' verdict when equal (most significant position outermost).
408def modelWord32OrderByte =
409 (lambda unrestricted left : Byte .
410 (lambda unrestricted right : Byte .
411 (lambda unrestricted equalResult : Nat .
412 (nat-eliminate
413 (lambda unrestricted less : Nat . Nat)
414 (nat-eliminate
415 (lambda unrestricted greater : Nat . Nat)
416 equalResult
417 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
418 (byte-less-than right left))
419 (lambda unrestricted predecessor : Nat .
420 (lambda unrestricted induction : Nat . (succ zero)))
421 (byte-less-than left right)))))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.