Re: [isabelle] Strictness



Hi Lutz,

[...]
However, one then runs across a somewhat
hidden feature: Sem_rel.intros mentions Sem_sumC, not Sem, and one needs
to unfold the definition of Sem in terms of Sem_sumC to make things work
as expected.

This is the construction the function package does internally to get rid
of mutual recursion and currying. It is a bit ugly...

Am I overlooking something? One sort of suspects that strictness
assertions such as the above might be available neatly packaged, say as
"Sem.strictness" or so...

No, this is not packaged, mainly because at the time I implemented it,
it was not clear what kind of rules are "the canonical thing that one
wants to have". Maybe such a packaging will be added at some point...

Alex






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.