[isabelle-dev] Tweak Haskell output for future Haskell compatibility.
makarius at sketis.net
Tue May 8 21:28:09 CEST 2012
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
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.
More information about the isabelle-dev