156def x86NativeSubtractByte =
157 (lambda unrestricted left : Byte .
158 (lambda unrestricted right : Byte .
159 (lambda unrestricted borrow : Nat .
160 (let unrestricted leftNatural =
161 (byte-to-nat left)
162 in
163 (let unrestricted rightNatural =
164 (x86NativeNaturalAdd (byte-to-nat right) borrow)
165 in
166 (let unrestricted outgoingBorrow =
167 (x86NativeNaturalPositive (x86NativeNaturalSubtract rightNatural leftNatural))
168 in
169 (nat-eliminate
170 (lambda unrestricted hasBorrow : Nat . (family X86NativeByteSubtractResult))
171 (constructor
172 X86NativeByteSubtractResult
173 X86NativeByteSubtractValue
174 (nat-to-byte (x86NativeNaturalSubtract leftNatural rightNatural))
175 zero)
176 (lambda unrestricted predecessor : Nat .
177 (lambda unrestricted induction : (family X86NativeByteSubtractResult) .
178 (constructor
179 X86NativeByteSubtractResult
180 X86NativeByteSubtractValue
181 (nat-to-byte
182 (x86NativeNaturalSubtract
183 (x86NativeNaturalAdd (succ (byte-to-nat (byte 255))) leftNatural)
184 rightNatural))
185 (succ zero))))
186 outgoingBorrow)))))))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.