Re: [isabelle] Isabelle style guide



> On 31.05.2015, at 09:02, C. Diekmann <diekmann at in.tum.de> wrote:
>
> 2015-05-30 23:09 GMT+02:00 Makarius <makarius at sketis.net>:
>> [...] Of
>> course that will be based on the good old standards, although I've found
>> myself doing a few things differently now, to optimize the content of the
>> first line of a specification, for the tree-view in SideKick.  E.g.
>>
>>  Bad:
>>
>>  definition foo :: T where
>>    "foo = ..."
>>
>>  definition
>>    bar :: T where
>>    "bar = ..."
>>
>>
>>  Good:
>>
>>  definition foobar :: T
>>    where "foobar = ..."
>
> 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.

Not even finished writing yet, and we have already started ;-)

âdefinition/where' is actually one of the case I'm having most trouble with.

Personally, I like the most line-consuming form:

definition
  foo :: T
where
  âfoo = barâ

because I tend to have long types and long definitions, sometimes both over multiple lines. The `where` in the same line as the definition adds noise to what Iâm most interested in (the definition itself).

The variant

definition foo :: T
where
  âfoo = barâ

works more nicely with folding.

definition foo :: "T => T => (some, other, 'params) list =>
                   T"
where
  âfoo = barâ

forces too much indentation for the line break.

Maybe the solution is simply to have both variants, the folding-friendly variant when everything fits on the line, the multi-line one, when it doesnât.

What do people think about this one for long types?

definition foo ::
  "T => T => (some, other, 'params) list => T"
where
  âfoo = barâ

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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