Re: [isabelle] Isabelle style guide



On Sun, 31 May 2015, C. Diekmann wrote:

When definitions get longer, the first bad version (subjectively)
appears more pleasant to me.

definition foo :: T where
 "foo = BlaulichtAufDerDatenautobahn"

definition foo :: T
 where "foo = BlaulichtAufDerDatenautobahn"

Putting the "where" in the first line saves space for the actual definition.

That is not a counter-example yet: the material after the 'where' can be broken up further, of course:

definition foo :: T
where
  "foo =
    let val x = long_material
    in multiple_lines x end"

There are many possibilities. The main purpose of the exercise is to follow these principles:

  * The first line is restricted to the most relevant information for
    SideKick tree view etc. (keyword 'where' is no relevant information).

  * The overall layout follows the structure of nesting and fits into the
    strict line length of 80-100 characters.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.