On Tue, 8 May 2012, Tobias Nipkow wrote:
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.
The expert(s) on code generation should comment on that, most notably
Florian.
When he made his first round on the renewed codegenerator, we changed a
few things at the bottom of the logic to get sort constraints out of the
way. As a consequence, primitive consts and corresponding definitional
axioms have become free from sort constraints, but the results are
presented to the user with constraints as expected.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
