Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- open import Agda.Builtin.Float
- record Colour : Set where
- constructor colour
- field
- r g b : Float
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement