Rodin Handbook


2.8.2 A Context with Colours

Start by creating a context called ctx1, as described in Section 2.6. We model the colours of the traffic light as a so-called “enumerated set” (3.3.4): We explicitly specify all elements (the three colours) of a new user-defined data type. We define the constants:


$\tt  red $
$\tt  yellow $
$\tt  green $

We introduce the new data type as a set:


$\tt  COLOURS $

And last, we need to provide typing of the constants. We do this by creating a partition (


$\tt  type :$

$\it  partition(COLOURS, \{  red\}  , \{  yellow\}  , \{  green\}  ) $


Please note the curly braces {} around the colours. It’s very easy to forget these, but if they are missing, typing errors will be displayed that are very hard for a novice to interpret.

This completes the context.