
10 Jul
2007
10 Jul
'07
4:05 p.m.
On 7/10/07, Andrew Coppin
But what does, say, "Maybe x -> x" say?
Maybe X is the same as "True or X", where True is the statement that is always true. Remember that the definition is data Maybe X = Nothing | Just X You can read | as 'or', 'Just' as nothing but a wrapper around an X and Nothing as an axiom. So Maybe X -> X says that "True or X" implies X. That's a valid proposition.