[Agda] signature for `with' branch

[Sergei Meshveliani]

On Mon, 2017-02-27 at 14:11 +0100, Nils Anders Danielsson wrote:
> On 2017-02-27 13:43, Sergei Meshveliani wrote:
> > Sometimes I manage to set a signature for `aux' in the branch.
> > Then, this helps a lot, because from `aux', the `with' sequence can be
> > started by new, and the problem is split to parts.
> 
> If this helps a lot, then I suggest that you do not use with at all. The
> with expressions are translated into regular Agda code, that you could
> have written yourself, with some exceptions, one of which is that with
> applications are not parsed (but they are not needed if you do not use
> with).
> 

I try to implement `lemma' from my last letter (see the code) without
using `with' or `case', and fail, so far:  

--------------------------------------------------------------
lemma :  ∀ a xs → a ≢ 0 → All (_≢ 0) xs → All (_≢ 0) (add a xs)

lemma a [] a≢0 _  with a ≟ 0
...               | yes _ = []a
...               | no _  = a≢0 ∷a []a

lemma a (x ∷ xs) a≢0 (x≢0 ∷a xs≢0) =  aux (a ≟ 0)
  where
  aux :  Dec (a ≡ 0) → All (_≢ 0) (add a (x ∷ xs))
  aux (yes a≡0) = ⊥-elim (a≢0 a≡0)
  aux (no a≢0)  = aux0 (compare a x)
      where
      aux0 : Tri (a < x) (a ≡ x) (a > x) → All (_≢ 0) (add a (x ∷ xs))
      aux0 (tri> _ _ _) = aux1 (a ≟ 0)
       	       	        where
       	       	        aux1 : Dec (a ≡ 0) → All (_≢ 0) (add a (x ∷ xs))
       	       	        aux1 (no _) =  a≢0 ∷a x≢0 ∷a xs≢0
---------------------------------------------------------------

The report is 

  a ∷ x ∷ xs != add a (x ∷ xs) | a Data.Nat.≟ 0 of type List ℕ
  when checking that the expression a≢0 ∷a x≢0 ∷a xs≢0 has type
  All (λ section → section ≢ 0) (add a (x ∷ xs))

And the pattern of  (tri> _ _ _) implies  the result of  (a ∷ x ∷ xs)
for `add'.

May be I also need to avoid `with' in the implementation of 'add' ?
Is this necessary?

------
Sergei