Source/Packages

Compiler.MachineX86NativeOffset

packages/compiler/src/Compiler/MachineX86NativeOffset.alpha

584 lines46 declarations23.5 KiBSHA-256 89175cb5d529

def · lines 543–561

x86NativeCountBytes32

Full file
543def x86NativeCountBytes32 : (pi unrestricted input : Bytes . (family X86NativeUnsigned32Result)) =
544  (lambda unrestricted input : Bytes .
545    (bytes-eliminate
546      (lambda unrestricted value : Bytes . (family X86NativeUnsigned32Result))
547      (constructor X86NativeUnsigned32Result X86NativeUnsigned32Success x86NativeUnsigned32Zero)
548      (lambda unrestricted head : Byte .
549        (lambda unrestricted tail : Bytes .
550          (lambda unrestricted induction : (family X86NativeUnsigned32Result) .
551            (eliminate
552              X86NativeUnsigned32Result
553              (lambda unrestricted result : (family X86NativeUnsigned32Result) .
554                (family X86NativeUnsigned32Result))
555              induction
556              (branch X86NativeUnsigned32Success value . (x86NativeIncrementUnsigned32 value))
557              (branch
558                X86NativeUnsigned32Overflow
559                .
560                (constructor X86NativeUnsigned32Result X86NativeUnsigned32Overflow))))))
561      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.