Type Checking
•
eval :: Term a
->
a
•
•
eval (Less x y) = eval x < eval y
•
•
•
Less::(a=Bool)=>Term Int -> Term Int -> Term Bool
•
•
x
:: Term Int
•
y
:: Term Int
•
(eval x)
:: Int
•
(eval y)
:: Int
•
(eval x < eval y) :: Bool
•
Assume a=Bool in this context