@@ -37,8 +37,8 @@ natToBin (S w) (S k) with (parity k)
3737 natToBin (S w) (S (plus j j)) | Even = do jbin <- natToBin w j
3838 let value = jbin # B1
3939 ?ntbEven
40− natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
41− let value = jbin # b0
40+ natToBin (S w) (S (S (plus j j))) | Odd = do jbin <- natToBin w (S j)
41+ let value = jbin # B0
4242 ?ntbOdd
4343
4444testBin : Maybe (Binary 8 42)
@@ -49,14 +49,14 @@ term syntax bitpair [x] [y] = (_ ** _ ** (x, y, Refl))
4949
5050addBit : Bit x -> Bit y -> Bit c ->
5151 (bX ** bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX))
52−addBit b0 b0 b0 = bitpair b0 b0
53−addBit b0 b0 b1 = bitpair b0 b1
54−addBit b0 b1 b0 = bitpair b0 b1
55−addBit b0 b1 b1 = bitpair b1 b0
56−addBit b1 b0 b0 = bitpair b0 b1
57−addBit b1 b0 b1 = bitpair b1 b0
58−addBit b1 b1 b0 = bitpair b1 b0
59−addBit b1 b1 b1 = bitpair b1 b1
52+addBit B0 B0 B0 = bitpair B0 B0
53+addBit B0 B0 B1 = bitpair B0 B1
54+addBit B0 B1 B0 = bitpair B0 B1
55+addBit B0 B1 B1 = bitpair B1 B0
56+addBit B1 B0 B0 = bitpair B0 B1
57+addBit B1 B0 B1 = bitpair B1 B0
58+addBit B1 B1 B0 = bitpair B1 B0
59+addBit B1 B1 B1 = bitpair B1 B1
6060
6161adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
6262adc Zero Zero carry ?= Zero # carry