[Agda] signature for `with' branch

[Sergei Meshveliani]

On Tue, 2017-02-28 at 11:26 +0100, Nils Anders Danielsson wrote:
> On 2017-02-27 21:38, Sergei Meshveliani wrote:
> > when I expect that there the result for  (add a (x ∷ xs))  must be
> > a ∷ x ∷ xs.
> 
> The term "add a (x ∷ xs)" reduces to "aux (a ≟ 0) (x ∷ xs)", which is
> stuck, because "a ≟ 0" does not reduce to WHNF.



> (I think you forgot to send the message to which I am responding to the
> mailing list.)


This is a test reply.
Sorry to disturb.

I copy it to  agda at lists.chalmers.se
and shall see whether it will come to me from the list. 

------
Sergei