[Agda] weird error with 'with'

[Nils Anders Danielsson]

On Sat, May 17, 2008 at 3:53 PM, Samuel Bronson <naesten at gmail.com> wrote:
>
> /home/naesten/hacking/haskell/proofs/lambda/Term.agda:67,7-13
> i + j != i of type ℕ
> when checking that the pattern ≡-refl has type
> .Relation.Binary.Core._≡_ (i + j + j') (i + (j + j'))

Agda cannot unify ((i + j) + j') and (i + (j + j')). Try abstracting
over one of the sides. See lem-plus-zero in Ulf's recent lecture
notes:

  http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.AFPSummerSchool2008

> P.S. Does anyone know how to get GNU Emacs 21 to copy/paste Unicode
> correctly under X?

Maybe you can get it to work if you set selection-coding-system
appropriately. Emacs 22 supports this out of the box, though, so I
would recommend you to upgrade.

-- 
/NAD