Re: [isabelle] Several questions about coding style/best practices



Ooh, a style bike-shed discussion :-)

I also strongly prefer the bracket style (for lemmas and theorems), because linear style becomes very hard to read for larger goals, but I use the linear (=> only) style for types, mostly because people are familiar with that from programming languages and types tend to not go over more than a line or two.

I use quotes for definitions, not cartouches, mostly because I’m used to it and it is fast to type, and I use cartouches for text and ML code, because I’m more likely to need to use quotes inside these.

Cheers,
Gerwin

> On 7 Jul 2019, at 22:04, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> I strongly prefer the bracketed style. The linear style is not very legible, especially when there is nesting.
> 
> But there are different points of view, and the bracket-style print mode is hard to access. To enable it, insert the line
> 
> JEDIT_PRINT_MODE=brackets
> 
> in your settings file.
> 
> Larry Paulson
> 
> 
> 
>> On 7 Jul 2019, at 12:42, mailing-list anonymous <mailing.list.anonymous at gmail.com> wrote:
>> 
>> I would like to clarify certain aspects related to the coding style best
>> suited for Isabelle2019. The question combines both my concerns about the
>> changes associated with the new release and, also, some of my previous
>> concerns. Unfortunately, I was not able to find an explicit Isabelle coding
>> style guide - please accept my apologies for asking this question if a
>> document that answers it already exists somewhere.
>> 
>> 1. Should ⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T) be preferred over S ⊆ 𝔘
>> ⟹ T ⊆ 𝔘 ⟹ τ S ⟹ τ T  ⟹ τ (S ∩ T)?
>> 2. Should ['a set, ('a set ⇒ bool), 'a set] ⇒ bool be preferred over 'a set
>> ⇒ ('a set ⇒ bool) ⇒ 'a set ⇒ bool?
> 
> 



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