Re: [isabelle] Isabelle style guide

On Sun, 31 May 2015, Gerwin Klein wrote:

Personally, I like the most line-consuming form:

 foo :: T
 âfoo = barâ

This form reminds me of ancient times of Proof General 2.0: head keyword standing alone, then the body below it. I can't remember why be converged to that in around 1999. Today I find it wasteful in vertical space, with these odd 16x9 displays. (Apart from the lack of relevant information in line 1 for SideKick.)

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
 âfoo = barâ

works more nicely with folding.

I am also using this routinely for anything that is not just very short. Putting the 'where' and the proposition on the same line is actually not so frequent, since real specifications don't fit there.

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

It fits into the principle of having relevant information on line 1, and breaking the rest according to normal indentation standards.

A definition and a theorem statement are analogous, and we already see things like this routinely:

theorem a: "short statement"

theorem b:
  "long statement
    broken into

theorem c:
  fixes ...
  assumes ...
  shows ...


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