[Agda] termination & open public

[Ulf Norell]

On Mon, Mar 17, 2008 at 9:48 PM, Ulf Norell <ulfn at cs.chalmers.se> wrote:

>
> On Mon, Mar 17, 2008 at 8:44 PM, Noam Zeilberger <noam+agda at cs.cmu.edu>
> wrote:
>
> > Is this a bug?  It seems that definitions exported by "open M public"
> > are not available to the termination checker.  Here is an example,
> > which is intended to capture some reasoning about the well-foundedness
> > of a subformula relationship:
>
>
> Yep, that's a bug. I'll look into it.
>

Fixed.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080317/94577c93/attachment.html