377def dataBytesCompare =
378 (lambda unrestricted left : Bytes .
379 (bytes-eliminate
380 (lambda unrestricted current : Bytes .
381 (pi unrestricted right : Bytes . (family DataBytesOrdering)))
382 (lambda unrestricted right : Bytes .
383 (bytes-eliminate
384 (lambda unrestricted current : Bytes . (family DataBytesOrdering))
385 (constructor DataBytesOrdering DataBytesEqual)
386 (lambda unrestricted rightHead : Byte .
387 (lambda unrestricted rightTail : Bytes .
388 (lambda unrestricted rightInduction : (family DataBytesOrdering) .
389 (constructor DataBytesOrdering DataBytesLess))))
390 right))
391 (lambda unrestricted leftHead : Byte .
392 (lambda unrestricted leftTail : Bytes .
393 (lambda unrestricted leftInduction : (pi unrestricted right : Bytes . (family DataBytesOrdering)) .
394 (lambda unrestricted right : Bytes .
395 (bytes-eliminate
396 (lambda unrestricted current : Bytes . (family DataBytesOrdering))
397 (constructor DataBytesOrdering DataBytesGreater)
398 (lambda unrestricted rightHead : Byte .
399 (lambda unrestricted rightTail : Bytes .
400 (lambda unrestricted rightInduction : (family DataBytesOrdering) .
401 (nat-eliminate
402 (lambda unrestricted current : Nat . (family DataBytesOrdering))
403 (nat-eliminate
404 (lambda unrestricted current : Nat . (family DataBytesOrdering))
405 (constructor DataBytesOrdering DataBytesGreater)
406 (lambda unrestricted lessPredecessor : Nat .
407 (lambda unrestricted lessInduction : (family DataBytesOrdering) .
408 (constructor DataBytesOrdering DataBytesLess)))
409 (byte-less-than leftHead rightHead))
410 (lambda unrestricted equalPredecessor : Nat .
411 (lambda unrestricted equalInduction : (family DataBytesOrdering) .
412 (leftInduction rightTail)))
413 (byte-equal leftHead rightHead)))))
414 right)))))
415 left))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.