•kind
Domain = High | Low
•
•data
D t
• = Lo where t = Low
• | Hi where t = High
•
•data
Dless x y
• = LH where x = Low , y = High
• | LL where x = Low, y = Low
• | HH where x = High, y = High
•
•data
Exp s d t
• = Int Int where t = Int
• | Bool Bool where t =
Bool
• | Plus (Exp s d Int) (Exp s d Int) where t =
Int
• | Lteq (Exp s d Int) (Exp s d Int) where t =
Bool
• | forall d2 . Var (V s d2 t) (Dless d2
d)
•