Re: [isabelle] Isabelle style guide



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.