*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] locales and 'types'*From*: Makarius <makarius at sketis.net>*Date*: Tue, 13 Jul 2010 13:35:03 +0200 (CEST)*In-reply-to*: <273BFF57-70DC-4D62-B4C3-A2F6B1136778@gmail.com>*References*: <2B597A2B-670A-41CD-916E-0F8291EEBD54@gmail.com> <alpine.LNX.1.10.1007131051320.22918@atbroy100.informatik.tu-muenchen.de> <273BFF57-70DC-4D62-B4C3-A2F6B1136778@gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Tue, 13 Jul 2010, Peter Gammie wrote:

I find this reasoning a bit confusing for "types" as 'a cannot be usedin the RHS anyway, i.e. this is illegal too:locale X = fixes a :: "'a" begin types Type = "'a set"It is not a construct that copes with things that are already fixed in acontext.

One more note on the example above. In order to avoid unnecessaryconfusion and unexpected problems, it is important to stick toestablished Isabelle naming conventions:* Theory names: capitalized words, typically describing the mainconceptin singular, e.g. "theory Foo_Bar_Concept" * Almost everything else in lower case, especially locale and type names. * Exceptions: capitalized datatype constructors, also some term constructions according to typical mathematical usage (e.g. capital singleton letters A, B, C, or occasional Foo for "sets" etc.)Could I humbly suggest that these and other style rules be put in adocument that accompanies the distribution?

Makarius

**References**:**[isabelle] locales and 'types'***From:*Peter Gammie

**Re: [isabelle] locales and 'types'***From:*Makarius

**Re: [isabelle] locales and 'types'***From:*Peter Gammie

- Previous by Date: Re: [isabelle] locales and 'types'
- Next by Date: Re: [isabelle] Finding the instantiation of a variable
- Previous by Thread: Re: [isabelle] locales and 'types'
- Next by Thread: Re: [isabelle] finite sets and code generation, once again
- Cl-isabelle-users July 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list