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

About typing speed: I usually adjust completion delay to 0, then the completions for abbreviations like cartouche when typing ", or symbols pops up immediately. However, to get semantic completions that come from pide then one has to wait and press ctrl-b.

Anyway, I find it more annoying to wait the default 0.5 seconds for any non ascii symbol, than not to have semantic completions without pressing a shortcut.


-------- Original Message --------
Subject: Re: [isabelle] Several questions about coding style/best practices
From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein at>
To: Lawrence Paulson <lp15 at>
CC: mailing-list anonymous <mailing.list.anonymous at>,cl-isabelle-users <cl-isabelle-users at>

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.


> On 7 Jul 2019, at 22:04, Lawrence Paulson 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
> in your settings file.
> Larry Paulson
>> On 7 Jul 2019, at 12:42, mailing-list anonymous 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.