Lambda functions miss the first pipe when formatted

[janmasrovira]

Example:

eq-lambda : Eq UNat :=
  mkEq
    λ{
      uzero uzero := true
      | (usuc n) (usuc m) := Eq.eq n m
      | _ _ := false
    };

In order to be consistent with other places where we also use pipes, it should be:

eq-lambda : Eq UNat :=
  mkEq
    λ{
      | uzero uzero := true
      | (usuc n) (usuc m) := Eq.eq n m
      | _ _ := false
    };

[lukaszcz]

Right, but if there is only one branch we shouldn't add a pipe, I think (so we have things like \{x := x + 1}).