[Agda] Sign.+ ◃

[Nils Anders Danielsson]

On 2013-11-14 15:37, Sergei Meshveliani wrote:
> I suspect that this is due to a particular pattern order in the
> implementation for  Integer._◃_.
> May be it is better to move the pattern with   ... zero
> to the second place?

I suggest that you try to implement this change, and evaluate it. I
suspect that one or more definitions in the standard library will break,
but perhaps others can be simplified.

-- 
/NAD