[isabelle-dev] Code export to Haskell and lower-case theory names
makarius at sketis.net
Tue Apr 2 12:38:30 CEST 2013
On Fri, 29 Mar 2013, Brian Huffman wrote:
>> Then it should be a hard rule enforced by the system. If that is not
>> the case, then it should be fully supported and up to the user to
>> choose his naming, even if it deviate from what others use (she might
>> have reasons for that).
> I completely agree.
Enforcing rules in a strict manner is always a very painful process.
We've done that over the years where it was absolutely necessary, e.g.
making the theorem name space conform to the policies of any other name
space (types, consts, etc.), despite all the complaints that were coming
from it. Now it is difficult to imagine that theorems would work
Generally, I see a variety of levels of checking by the system, a spectrum
between enforcement to encourgement: error, warning, hilighting. BTW, in
Isabelle/jEdit a plain warning already looks quite prominent.
More information about the isabelle-dev