[Agda] running out of memory in formalization of category theory

[Nils Anders Danielsson]

On 2010-06-06 22:28, Nicolas Pouillard wrote:
> To workaround any of the two situations one can keep both the concrete
> version and the abstract one.
>
> <  concrete-foo : Bar
> <  concrete-foo = ...
> <
> <  abstract
> <    foo : Bar
> <    foo = concrete-foo
>
> This may suggest a finer-grained support at the term level, where we could
> make abstract a name in a term.
>
> <  term ::= ... | abstract name
>
> Using this, `abstract foo' is almost like `foo' (same type and definition)
> but can only be compared by its name and so will only be equal to itself.
>
> What do you think?

I would rather see effort being spent on making Agda faster, than on
constructing crutches to avoid the current poor performance.

-- 
/NAD