441def stdI32LessThan =
442 (lambda unrestricted a : (family StdI32) .
443 (lambda unrestricted b : (family StdI32) .
444 (nat-eliminate
445 (lambda unrestricted current : Nat . Nat)
446 (nat-eliminate
447 (lambda unrestricted current : Nat . Nat)
448 (stdU32LessThan (stdI32ToWord a) (stdI32ToWord b))
449 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
450 (stdU32HighBit (stdI32ToWord b)))
451 (lambda unrestricted predecessor : Nat .
452 (lambda unrestricted induction : Nat .
453 (nat-eliminate
454 (lambda unrestricted current : Nat . Nat)
455 (succ zero)
456 (lambda unrestricted predecessorB : Nat .
457 (lambda unrestricted inductionB : Nat .
458 (stdU32LessThan (stdI32ToWord a) (stdI32ToWord b))))
459 (stdU32HighBit (stdI32ToWord b)))))
460 (stdU32HighBit (stdI32ToWord a)))))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.