@@ -37,8 +37,8 @@ natToBin (S w) (S k) with (parity k)
37 natToBin (S w) (S (plus j j)) | Even = do jbin <- natToBin w j
37 natToBin (S w) (S (plus j j)) | Even = do jbin <- natToBin w j
38 let value = jbin # B1
38 let value = jbin # B1
40− natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
40+ natToBin (S w) (S (S (plus j j))) | Odd = do jbin <- natToBin w (S j)
41− let value = jbin # b0
41+ let value = jbin # B0
44testBin : Maybe (Binary 8 42)
44testBin : Maybe (Binary 8 42)
@@ -49,14 +49,14 @@ term syntax bitpair [x] [y] = (_ ** _ ** (x, y, Refl))
50addBit : Bit x -> Bit y -> Bit c ->
50addBit : Bit x -> Bit y -> Bit c ->
51 (bX ** bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX))
51 (bX ** bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX))
52−addBit b0 b0 b0 = bitpair b0 b0
52+addBit B0 B0 B0 = bitpair B0 B0
53−addBit b0 b0 b1 = bitpair b0 b1
53+addBit B0 B0 B1 = bitpair B0 B1
54−addBit b0 b1 b0 = bitpair b0 b1
54+addBit B0 B1 B0 = bitpair B0 B1
55−addBit b0 b1 b1 = bitpair b1 b0
55+addBit B0 B1 B1 = bitpair B1 B0
56−addBit b1 b0 b0 = bitpair b0 b1
56+addBit B1 B0 B0 = bitpair B0 B1
57−addBit b1 b0 b1 = bitpair b1 b0
57+addBit B1 B0 B1 = bitpair B1 B0
58−addBit b1 b1 b0 = bitpair b1 b0
58+addBit B1 B1 B0 = bitpair B1 B0
59−addBit b1 b1 b1 = bitpair b1 b1
59+addBit B1 B1 B1 = bitpair B1 B1
61adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
61adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
62adc Zero Zero carry ?= Zero # carry
62adc Zero Zero carry ?= Zero # carry