251def modelWord64OrderByte =
252 (lambda unrestricted left : Byte .
253 (lambda unrestricted right : Byte .
254 (lambda unrestricted equalResult : Nat .
255 (nat-eliminate
256 (lambda unrestricted less : Nat . Nat)
257 (nat-eliminate
258 (lambda unrestricted greater : Nat . Nat)
259 equalResult
260 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
261 (byte-less-than right left))
262 (lambda unrestricted predecessor : Nat .
263 (lambda unrestricted induction : Nat . (succ zero)))
264 (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.