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



I agree with Larry about brackets, but acknowledge that's personal preference. I know many people who prefer linear mode.

BTW the print mode is also accessible in jedits option menu, use plugins isabelle general options and look for the print mode field.

Peter


-------- Original Message --------
Subject: Re: [isabelle] Several questions about coding style/best practices
From: Lawrence Paulson <lp15 at cam.ac.uk>
To: mailing-list anonymous <mailing.list.anonymous at gmail.com>
CC: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>


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 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.