[isabelle] Fwd: Isabelle style guide
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Fwd: Isabelle style guide
- From: Christine Sherif Rizkallah <christine2711987 at gmail.com>
- Date: Tue, 2 Jun 2015 16:11:59 +1000
- In-reply-to: <CAOu=+dZ9NHdHZe61K4J=8it-_sgVy9kH6qD2MWX5bHJvJzdLFA@mail.gmail.com>
- References: <9ACE55FB-A37E-4A63-BF9C-5F484ECBF8E2@nicta.com.au> <alpine.LNX.firstname.lastname@example.org> <E0896D6C-CD27-4F5A-ADF3-6E573E18B3CF@nicta.com.au> <alpine.LNX.email@example.com> <556C5CC1.firstname.lastname@example.org> <CAOu=+dZ9NHdHZe61K4J=8it-_sgVy9kH6qD2MWX5bHJvJzdLFA@mail.gmail.com>
foo :: T
âfoo = barâ
Its nice to have a line to separate the type and the actual definition.
A more important issue though is recommending always explicitly writing the
On Mon, Jun 1, 2015 at 11:23 PM, Lars Noschinski <noschinl at in.tum.de> wrote:
> On 30.05.2015 23:09, Makarius wrote:
> > Bad:
> > definition foo :: T where
> > "foo = ..."
> This is the form I use most. It only uses two lines and keeps as much
> space as possible for the actual definition. I don't mind seeing the
> unnecessary "where" in the sidekick -- it is at the end of the line,
> after all. Also, seeing the name suffices for my purposes, so even the
> type is unnecessary (for me).
> I mostly use the sidekick to see the section structure. I would like to
> see more information about my lemmas there (instead of just the name),
> but I almost always state my lemmas in structured form, so I have a line
> break after name.
> -- Lars
This archive was generated by a fusion of
Pipermail (Mailman edition) and