Source/Packages

Compiler.MachineX86NativeOffset

packages/compiler/src/Compiler/MachineX86NativeOffset.alpha

584 lines46 declarations23.5 KiBSHA-256 89175cb5d529

def · lines 563–584

x86NativeAdvanceUnsigned32ByBytes

Full file
563def x86NativeAdvanceUnsigned32ByBytes :
564  (pi unrestricted initial : (family X86NativeUnsigned32) .
565    (pi unrestricted input : Bytes . (family X86NativeUnsigned32Result))) =
566  (lambda unrestricted initial : (family X86NativeUnsigned32) .
567    (lambda unrestricted input : Bytes .
568      (bytes-eliminate
569        (lambda unrestricted value : Bytes . (family X86NativeUnsigned32Result))
570        (constructor X86NativeUnsigned32Result X86NativeUnsigned32Success initial)
571        (lambda unrestricted head : Byte .
572          (lambda unrestricted tail : Bytes .
573            (lambda unrestricted induction : (family X86NativeUnsigned32Result) .
574              (eliminate
575                X86NativeUnsigned32Result
576                (lambda unrestricted result : (family X86NativeUnsigned32Result) .
577                  (family X86NativeUnsigned32Result))
578                induction
579                (branch X86NativeUnsigned32Success value . (x86NativeIncrementUnsigned32 value))
580                (branch
581                  X86NativeUnsigned32Overflow
582                  .
583                  (constructor X86NativeUnsigned32Result X86NativeUnsigned32Overflow))))))
584        input)))

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.