[Agda] termination check

[Andrés Sicard-Ramírez]

It seems you need to add to the module A the instruction

{-# OPTIONS --no-termination-check #-}


On Fri, Nov 27, 2009 at 4:51 AM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> Hello.
>
> I had a big agda file with one function that doesn't temination-checks (and
> that's the way things should be). But apart from this check everything went
> ok, as expected. Now I decided to split this into several modules, and I get
> a problem: when I compile (from emacs) module B which uses A, the
> compilation complains that A doesn't termination check and stops. The
> compilation of A is fine, apart from the termination checking. How should I
> proceed to be able to compile B (i.e., how do I make agda "trust me" on this
> one?)
>
> Thanks.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Andrés