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

[Dan Licata]

Ooh, I didn't know that multiple abstract blocks in the same module
could see each other.  That actually solves a problem I had: I wanted to
define an abstract function, then a transparent definition, then an
abstract definition that dependend on both the abstract function and the
transparent definition.  In ML terms, I wanted a signature like

type t
type d = t -> t
val  x : d  -- implementation needs to know implementation of t

but before I knew that multiple abstract blocks could see each other, it
didn't seem like there was a way to do it---except inlining the
definition of d in the type of x, and then defining d later (in the
actual example the term being abbreviated was much longer).

-Dan

On Jun07, Nils Anders Danielsson wrote:
> On 2010-06-06 19:49, kahl at cas.mcmaster.ca wrote:
> >Is there more documentation of ``abstract'' anywhere?
> 
> I don't think there is any formal definition of what "abstract" means. I
> also regard it as rather experimental and ad-hoc, and try to avoid using
> it if I can, in the hope that a cleaner alternative will eventually
> emerge.
>