11 Sep
2006
11 Sep
'06
3:07 p.m.
On 9/11/06, Bulat Ziganshin <bulat.ziganshin@gmail.com> wrote:
Expr Bool = Eq (Expr t) (Expr t) | forall t . Eq t
Still confusing, but less so. The problem is that it's really backwards. The symbol being defined is "Eq". Eq (Expr t) (Expr t) | Eq t = Expr Bool but that doesn't fit well, does it? In my mind, the current mode is a functional one: Eq :: Eq t => Expr t -> Expr t -> Expr Bool And this is perfectly readable. The arrow means that the argument is an implicit propositional one, but it's still an argument. -- Taral <taralx@gmail.com> "You can't prove anything." -- Gödel's Incompetence Theorem