3 ms·

let Sub = λ a b f c.b (\ x.x True) (a (\ cc o.o cc (f (cc False))) (λ o.o c c)) False Subtraction is always fun.

• Joker_vD 2y ago
  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.