[isabelle] Fwd: Isabelle style guide



definition
 foo :: T
where
 â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
types.



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