Theorem types should be on new lines

[JasonGross]

If the entire type of a theorem or definition does not fit on one line, then it is better to put the result type (the part after the colon) on an indented line by itself, together with the colon to make it clear that this is the result type.

   Definition triangulator {A : Type} {x y z : A} (p : x = y) (q : y = z)
     : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q.

We should do this consistently throughout the library.

[vladimirias]

I am interested in having this also consistent with how we do it in UniMath. Currently (in the new work I sill have to go back to old material in Foundations and make the lines shorter there) I was doing this:

Definition towerfunontowersovers { n : nat } { T T' : tower } ( f : towerfun T T' ) ( G : T n ) : towerfun ( tfib G ) ( tfib ( f n G ) ) := towerfuntfib ( nshiftfunct n f ) G .

... and also this:

CoFixpoint towerstrmap ( T : tower ) ( t0 : pr0 T ) : towerfun ( tfib t0 ) T := towerfunconstr ( fun x => t0 ) ( fun t1 => towerstrmap ( tfib t0 ) t1 ) .

I think it is probably a little more close to the writing style to keep the : before the line break. It's like I would write

For example:

.....

V.

On Oct 10, 2014, at 7:46 AM, Jason Gross notifications@github.com wrote:

If the entire type of a theorem or definition does not fit on one line, then it is better to put the result type (the part after the colon) on an indented line by itself, together with the colon to make it clear that this is the result type.

Definition triangulator {A : Type} {x y z : A} (p : x = y) (q : y = z) : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q. We should do this consistently throughout the library.

— Reply to this email directly or view it on GitHub.

[mikeshulman]

I feel fairly strongly that the : and := should be after the line break, so that you can tell immediately on which line begins the result type and on which line begins the definition. The beginnings of lines are much more obvious than the ends.

[spitters]

I agree. Some people have the same conventions wrt ; for e.g. record types.

Class Modality :=
{ mod_usubu : UnitSubuniverse
; mod_replete : Replete mod_usubu
; O_rect : forall A (B : O A -> Type) (B_inO : forall oa, inO (B oa)),
 (forall a, B (O_unit A a)) -> forall a, B a
; O_rect_beta : forall A B B_inO (f : forall a : A, B (O_unit A a)) a,
  O_rect A B B_inO f (O_unit A a) = f a
; inO_paths : forall A (A_inO : inO A) (z z' : A), inO (z = z') }.

vs what we have now

Class Modality := { mod_usubu : UnitSubuniverse ; mod_replete : Replete mod_usubu ; O_rect : forall A (B : O A -> Type) (B_inO : forall oa, inO (B oa)), (forall a, B (O_unit A a)) -> forall a, B a ; O_rect_beta : forall A B B_inO (f : forall a : A, B (O_unit A a)) a, O_rect A B B_inO f (O_unit A a) = f a ; inO_paths : forall A (A_inO : inO A) (z z' : A), inO (z = z') }.

We could try to teach coq_indenter or coq's beautify to do these things for us if we feel very strongly about this.

On Fri, Oct 10, 2014 at 9:13 PM, Mike Shulman notifications@github.com wrote:

I feel fairly strongly that the : and := should be after the line break, so that you can tell immediately on which line begins the result type and on which line begins the definition. The beginnings of lines are much more obvious than the ends.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/564#issuecomment-58702993.

[andrejbauer]

I personally prefer Vladimir's style, but I also see the benefit of the standard adopted in the HoTT library. The thing with records that Bas suggests is not something I'd do either, and I think Haskell people who write

do { foo
   ; bar
   ; baz
   }

are weird.