let True = t f. t
let False = t f. f
let not = x. x False True
let Byte = b7 b6 b5 b4 b3 b2 b1 b0. f. f b7 b6 b5 b4 b3 b2 b1 b0
let xor3 = a b c. a (b c (not c)) (b (not c) c)
let maj3 = a b c. a (b True c) (b c False)
let full_adder = a b c k. k (xor3 a b c) (maj3 a b c)
let adc = a b ci k. a (b (
b7 b6 b5 b4 b3 b2 b1 b0. (
a7 a6 a5 a4 a3 a2 a1 a0. (
full_adder a0 b0 ci (s0 c0.
full_adder a1 b1 c0 (s1 c1.
full_adder a2 b2 c1 (s2 c2.
full_adder a3 b3 c2 (s3 c3.
full_adder a4 b4 c3 (s4 c4.
full_adder a5 b5 c4 (s5 c5.
full_adder a6 b6 c5 (s6 c6.
full_adder a7 b7 c6 (s7 c7.
k (Byte s7 s6 s5 s4 s3 s2 s1 s0) c7
))))))))))))
let inv = b. b (b7 b6 b5 b4 b3 b2 b1 b0.
Byte (not b7) (not b6) (not b5) (not b4) (not b3) (not b2) (not b1) (not b0))
let sub = a b. adc a (inv b) True (s _. s)
let Zero = z i. z
let Int = lsb rest. z i. i (lsb rest)
Extending the subtraction to the bigints represented as little-endian lists of bytes is left as an exercise to the reader.
P.S. De we really need a leading \ or λ for the lambda-abstraction? I personally think the dot is quite unambiguous and clear on its own.
P.S. De we really need a leading \ or λ for the lambda-abstraction? I personally think the dot is quite unambiguous and clear on its own.