[Agda] signature for `with' branch

Nils Anders Danielsson nad at cse.gu.se
Tue Feb 28 11:26:57 CET 2017


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.)

-- 
/NAD


More information about the Agda mailing list