Skip to main content

Color

inductive Color {
    red
    green
    blue
}

A simple enumeration type used as an example of a metric space with the discrete metric.

GitHub

blue​

Color.blue: Color

Blue is not red or green.

green​

Color.green: Color

Green is not red or blue.

red​

Color.red: Color

Red means nothing. It's just different from green and blue.