Std.Byte

28def byteAdd =
29  (lambda unrestricted left : Byte .
30    (lambda unrestricted right : Byte .
31      (app
32        (lambda unrestricted total : Nat .
33          (constructor
34            ByteAddResult
35            ByteAddResultValue
36            -- total is in 0..510. The primitive conversion keeps its low
37            -- eight bits, and its high part is exactly the flag total > 255.
38            -- Avoid general unary division/modulo in this bounded operation.
39            (nat-to-byte total)
40            (nat-less-than (byte-to-nat (byte 255)) total)))
41        (naturalAdd (byte-to-nat left) (byte-to-nat right)))))