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



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.