Re: [isabelle] Several questions about coding style/best practices
- To: mailing-list anonymous <mailing.list.anonymous at gmail.com>
- Subject: Re: [isabelle] Several questions about coding style/best practices
- From: Lawrence Paulson <lp15 at cam.ac.uk>
- Date: Sun, 7 Jul 2019 13:04:39 +0100
- Cc: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- In-reply-to: <CALaF1UJQ_Dfg26rFY=CRFhh4jHf9zM3G-ChaZ3cwtnN3p3iT-Q@mail.gmail.com>
- References: <CALaF1UJQ_Dfg26rFY=CRFhh4jHf9zM3G-ChaZ3cwtnN3p3iT-Q@mail.gmail.com>
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.
> 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