Proposal for separating patterns in Style convention

[mechvel]

I suggest to allow some more separator for the lines of patterns in the same function and between function bodies.
Because it is very difficult to read the source code in lib-1.2.
Function bodies look somewhat like this:

f pattrern1 ... =  ...
  where
  def1 ...
  def-n ...
f pattern2 ... = ....
  where
  ...

g : ...

The bodies for (f pattern1), (f pattern2) ... often have long lines and are pressed to each other.
So that it is difficult to observe where there starts the body of the next pattern.
I suggest to allow to insert empty line between the body of the pattern and the head of the next pattern of the same function.
If this is allowed, then we also need to allow to insert one more empty line after the body of each (upper level) function.
This will make observing/reading of the source much easier.

[MatthewDaggitt]

I have noticed that you tend to write very large proofs, and I agree the extra whitespace can be useful in these. However I would guesstimate that over 90% of the proofs in the standard library are 6 lines or less. So from my perspective this would introduce a lot of extra whitespace throughout the library for a minor gain in a small number of proofs.

Additionally, (although more of an observation rather than a convincing argument) I haven't seen many other people using the style you're advocating. The style used in the standard library is much more common amongst other people's code.

Open to being convinced though. Does anyone else have any opinions?

[mechvel]

Indeed, for the most of the code in lib-1.2 my suggestion does not help.
But many proofs for new Binary (for its _<_ properties, proofs in Minus.agda) are difficult to read - due to that data representation is more complex than, say, for Integer.
Look into Nat.Binary.Properties, Minus.agda of December 23.
And I only suggest to allow (not to demand) extra empty line, - and may be, more freedom in indentation, - when many long pattern statements are pressed to each other. This will be on the programmer to decide about extra line.

As to lib-1.2, consider Integer.Properties.∣m-n∣≡∣n-m∣,
and let it be followed by a certain contrived ∣m-n∣≡∣foo
(but I fail to fix indentation in this editor !!):

∣m-n∣≡∣n-m∣ : (x y : ℤ) → ∣ x - y ∣ ≡ ∣ y - x ∣ 
∣m-n∣≡∣n-m∣ -[1+ x ] -[1+ y ] = ∣m⊖n∣≡∣n⊖m∣ y x 
∣m-n∣≡∣n-m∣ -[1+ x ] (+ y)    = begin 
  ∣ -[1+ x ] - (+ y) ∣   ≡⟨ cong ∣_∣ (neg-minus-pos x y) ⟩                        
  suc (y ℕ.+ x)         ≡⟨ sym (ℕₚ.+-suc y x) ⟩                                  
  y ℕ.+ suc x           ∎ where open ≡-Reasoning                                 
∣m-n∣≡∣n-m∣ (+ x)    -[1+ y ] = begin                                             
  x ℕ.+ suc y              ≡⟨ ℕₚ.+-suc x y ⟩                                        
  suc (x ℕ.+ y)            ≡⟨ cong ∣_∣ (sym (neg-minus-pos y x)) ⟩                  
  ∣ -[1+ y ] + - (+ x) ∣   ∎ where open ≡-Reasoning                                 
∣m-n∣≡∣n-m∣ (+ x)     (+ y) = begin                                               
  ∣ (+ x) - (+ y) ∣ ≡⟨ cong ∣_∣ ([+m]-[+n]≡m⊖n x y) ⟩                             
  ∣ x ⊖ y ∣         ≡⟨ ∣m⊖n∣≡∣n⊖m∣ x y ⟩                                          
  ∣ y ⊖ x ∣         ≡⟨ cong ∣_∣ (sym ([+m]-[+n]≡m⊖n y x)) ⟩                       
  ∣ (+ y) - (+ x) ∣ ∎ where open ≡-Reasoning                                      

∣m-n∣≡∣foo : (x y : ℤ) → ∣ x - y ∣ ≡ foo
∣m-n∣≡∣n-m∣ -[1+ x ] -[1+ y ] = ∣m⊖n∣≡∣n⊖m∣ y x
∣m-n∣≡∣n-m∣ -[1+ x ] (+ y)    = m-n∣≡∣n-m∣ -[1+ x ] (foo' (+ y))

With the suggested style, it is possible to write
(but I fail to indent things in this editor! please, imagine that they are indented).

∣m-n∣≡∣n-m∣ : (x y :  ℤ) → ∣ x - y ∣ ≡ ∣ y - x ∣    -- signature is more important than 
                                                -- implementation, _allow_ to separate it
∣m-n∣≡∣n-m∣ -[1+ x ] -[1+ y ] = ∣m⊖n∣≡∣n⊖m∣ y x 
∣m-n∣≡∣n-m∣ -[1+ x ] (+ y)    =
  begin ∣ -[1+ x ] - (+ y) ∣    ≡⟨ cong ∣_∣ (neg-minus-pos x y) ⟩ 
           suc (y ℕ.+ x)            ≡⟨ sym (ℕₚ.+-suc y x) ⟩ 
           y ℕ.+ suc x
  ∎ where open ≡-Reasoning
  
∣m-n∣≡∣n-m∣ (+ x) -[1+ y ] =  
            begin x ℕ.+ suc y              ≡⟨ ℕₚ.+-suc x y ⟩  
                      suc (x ℕ.+ y)            ≡⟨ cong ∣_∣ (sym (neg-minus-pos y x)) ⟩  
                      ∣ -[1+ y ] + - (+ x) ∣ 
           ∎ where open ≡-Reasoning           

∣m-n∣≡∣n-m∣ (+ x) (+ y) =
          begin ∣ (+ x) - (+ y) ∣    ≡⟨ cong ∣_∣ ([+m]-[+n]≡m⊖n x y) ⟩ 
                    ∣ x ⊖ y ∣            ≡⟨ ∣m⊖n∣≡∣n⊖m∣ x y ⟩ 
                    ∣ y ⊖ x ∣            ≡⟨ cong ∣_∣ (sym ([+m]-[+n]≡m⊖n y x)) ⟩ 
                    ∣ (+ y) - (+ x) ∣
          ∎ where open ≡-Reasoning                
                                                              -- two emptylines allowed
                                                              --
∣m-n∣≡∣foo : (x y : ℤ) → ∣ x - y ∣ ≡ foo
∣m-n∣≡∣n-m∣ -[1+ x ] -[1+ y ] = ∣m⊖n∣≡∣n⊖m∣ y x
∣m-n∣≡∣n-m∣ -[1+ x ] (+ y)    = m-n∣≡∣n-m∣ -[1+ x ] (foo' (+ y))

(but this code is simpler than in Nat.Binary).
Just to grant a bit more freedom for empty lines and indentation.

I agree that it makes sense to consider formatting on a case‐by‐case basis. I think large definitions can benefit from the empty lines, whereas short ones can benefit from being more concise.

[mechvel]

May be, a line of dashes, for the extra line.
For example, the current style is

2[1+ x ] ∸ 1+[2 y ] with foo1 foo foo foo foo foo foo foo foo
... | yes _ =  foo1 foo foo foo foo foo foo foo foo foo foo foo                                                          
... | no _  = 1+[2 ( foo1 foo foo foo foo foo foo foo foo foo foo) ]                                      
1+[2 x ] ∸ 2[1+ y ] with  foo1 foo foo foo foo foo foo foo foo 
... | yes _ = foo2 foo foo foo foo foo foo foo foo foo foo foo

An extra empty line will help.
But if so, then the next function to this one needs to be separated with two empty lines.

[mechvel]

I have noticed that you tend to write very large proofs, and I agree the extra whitespace can be
useful in these.
[..]

I do not like large proofs, but I often fail to make them smaller. For example, representing Bin with three constructors increases the number of patterns and the patterns themselves. Another source may be a care for not spoiling performance.