[Agda] Refectoring Builtins

[Ulf Norell]

On Mon, Sep 13, 2010 at 6:05 PM, Simon Foster <s.foster at dcs.shef.ac.uk>wrote:

> Hi,
>
> What's the best place to store new builtin definitions? At the moment I've
> got them as an additional field in TCState, which seems to be the easiest.
> I've then altered resetState to make this new field persistent between
> reloads, as I notice you're already doing with command-line options - is
> this acceptable?
>

Yes, that makes sense.


> I'll also need an additional field to store external tool functions
> (something like [[String] -> Term -> TCM Term]).
>

Is this be for function that should be run during type checking? Can't you
just use primitives for those?

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100913/779f8c56/attachment.html