486def x86NativeRelativeDisplacement :
487 (pi unrestricted target : (family X86NativeUnsigned32) .
488 (pi unrestricted sourceEnd : (family X86NativeUnsigned32) .
489 (family X86NativeRelativeDisplacementResult))) =
490 (lambda unrestricted target : (family X86NativeUnsigned32) .
491 (lambda unrestricted sourceEnd : (family X86NativeUnsigned32) .
492 (eliminate
493 X86NativeUnsigned32SubtractResult
494 (lambda unrestricted result : (family X86NativeUnsigned32SubtractResult) .
495 (family X86NativeRelativeDisplacementResult))
496 (x86NativeSubtractUnsigned32 target sourceEnd)
497 (branch
498 X86NativeUnsigned32SubtractValue
499 forwardDifference
500 borrow
501 .
502 (nat-eliminate
503 (lambda unrestricted negative : Nat . (family X86NativeRelativeDisplacementResult))
504 (nat-eliminate
505 (lambda unrestricted inRange : Nat . (family X86NativeRelativeDisplacementResult))
506 (constructor
507 X86NativeRelativeDisplacementResult
508 X86NativeRelativeDisplacementOutOfRange)
509 (lambda unrestricted predecessor : Nat .
510 (lambda unrestricted induction : (family X86NativeRelativeDisplacementResult) .
511 (constructor
512 X86NativeRelativeDisplacementResult
513 X86NativeRelativeDisplacementSuccess
514 forwardDifference)))
515 (x86NativePositiveRel32 forwardDifference))
516 (lambda unrestricted predecessor : Nat .
517 (lambda unrestricted induction : (family X86NativeRelativeDisplacementResult) .
518 (eliminate
519 X86NativeUnsigned32SubtractResult
520 (lambda unrestricted reverseResult : (family X86NativeUnsigned32SubtractResult) .
521 (family X86NativeRelativeDisplacementResult))
522 (x86NativeSubtractUnsigned32 sourceEnd target)
523 (branch
524 X86NativeUnsigned32SubtractValue
525 magnitude
526 reverseBorrow
527 .
528 (nat-eliminate
529 (lambda unrestricted inRange : Nat .
530 (family X86NativeRelativeDisplacementResult))
531 (constructor
532 X86NativeRelativeDisplacementResult
533 X86NativeRelativeDisplacementOutOfRange)
534 (lambda unrestricted rangePredecessor : Nat .
535 (lambda unrestricted rangeInduction : (family X86NativeRelativeDisplacementResult) .
536 (constructor
537 X86NativeRelativeDisplacementResult
538 X86NativeRelativeDisplacementSuccess
539 (x86NativeNegateUnsigned32 magnitude))))
540 (x86NativeNegativeMagnitudeRel32 magnitude))))))
541 borrow)))))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.