Am 08/05/2012 14:44, schrieb Makarius: > So apart from the observation that the foundational kernel does not require > sort > constraints (apart from HOL.type of course), were there any reasons against > them?
They are not allowed in Haskell anymore, so why do we allow them (and complicate the code generation for Haskell in the future)? That was the starting point. That the kernel does not require sort constraints is not the point. Even if it did, you would still not need sort constraints in datatypes because their construction does not involve any sorts. You could always (I think) define an unconstrained datatype, even if its intended usage is in a constrained setting. I now see that there are certain extra-logical uses and accept that some people just like to explicitly constrain the usage of a datatype. Now that the machinery works smoothly, I would not suggest to remove it. Tobias _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
