[Agda] "abstract," Integer, and errors

[Nils Anders Danielsson]

On Tue, Jun 17, 2008 at 10:25 AM, Sean Leather <sean.leather at gmail.com> wrote:
>
> First, I tried (using the Emacs mode) to generate the case patterns. I got
> the following error:
>
>   Panic: NotADatatype (El (Type 0) (Def Data.Integer.Integer [])).

The integers are abstract, so you cannot pattern match on them. (And
apparently Agda panics instead of generating a suitable error
message.)

> So, Z is abstract and I can't pattern match on it. I'm fine with that,
> though I would like to know why this is the case.

I think that the original idea was to make Z abstract (hiding the
implementation details, to make it possible to switch to a more
efficient implementation in the future), but provide some sort of
generally useful interface. However, I never got this far. You may be
the first person who have actually used Data.Integer.

I have now made the definitions concrete.

-- 
/NAD