[Agda] termination & open public

[Ulf Norell]

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.

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