7 | data Color : Type where
13 | MkRGBA : (r : Int) -> (g : Int) -> (b : Int) -> (a : Int) -> Color
18 | MkRGB : (r : Int) -> (g : Int) -> (b : Int) -> Color
23 | rgbaOfColor : (color : Color) -> (Int,Int,Int,Int)
24 | rgbaOfColor (MkRGB r g b) = (r,g,b,255)
25 | rgbaOfColor (MkRGBA r g b a) = (r,g,b,a)
29 | a == b = rgbaOfColor a == rgbaOfColor b
30 | a /= b = not (a == b)
37 | addColors : (c1 : Color) -> (c2 : Color) -> Color
39 | let (r1, g1, b1, a1) = rgbaOfColor c1
40 | (r2, g2, b2, a2) = rgbaOfColor c2
41 | in MkRGBA (r1 + r2) (g1 + g2) (b1 + b2) ((a1 + a2) `div` 2)
47 | transparent = MkRGBA 0 0 0 0
51 | white = MkRGB 255 255 255
63 | green = MkRGB 0 255 0
67 | blue = MkRGB 0 0 255
71 | yellow = MkRGB 255 255 0
75 | magenta = MkRGB 255 0 255
79 | cyan = MkRGB 0 255 255