[Agda] Type unification problem in Braun Tree

[Nils Anders Danielsson]

On 05/11/08 05:35, Liang-Ting Chen wrote:

> We could know whether a BTree is a <_,_,_>-0 or <_,_,_>-1 by its parity, 

If you want to take advantage of this, then I suggest that you index
your trees on a number type which exposes the parity in a constructor
which you can easily pattern match on. Binary numbers with the least
significant digit at the top should do (see Data.Bin).

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.