88def byteAddWithCarry =
89 (lambda unrestricted left : Byte .
90 (lambda unrestricted right : Byte .
91 (lambda unrestricted carry : Nat .
92 (eliminate
93 ByteAddResult
94 (lambda unrestricted current : (family ByteAddResult) . (family ByteAddResult))
95 (byteAdd left right)
96 (branch
97 ByteAddResultValue
98 firstLow
99 firstCarry
100 .
101 (eliminate
102 ByteAddResult
103 (lambda unrestricted current : (family ByteAddResult) . (family ByteAddResult))
104 (byteAdd firstLow (nat-to-byte carry))
105 (branch
106 ByteAddResultValue
107 secondLow
108 secondCarry
109 .
110 (constructor
111 ByteAddResult
112 ByteAddResultValue
113 secondLow
114 (naturalAdd firstCarry secondCarry)))))))))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.