[Agda] not strictly positive?! I don't believe it!

[Andreas Abel]

Hi David,

On Sep 20, 2010, at 1:34 PM, David Leduc wrote:
> --According to the type checker, the T below is not strictly positive.
> --But I don't believe it.

Me neither. ;-)

> --Is it a bug?

Well, the positivity checker is only a sound approximation to the  
semantic concept of "strict positivity".

> --If not, can I force Agda to accept this definition anyway?

Add

   {-# OPTIONS --no-positivity-check #-}

to the top of your file.

>
> module test where
>
> open import Coinduction
>
> data unit : Set where
>  * : unit
>
> mutual
>  data T : Set1 where
>    intro : (t : ∞ T) -> [ ♭ t ] -> T
>
>  [_] : T -> Set
>  [ intro _ _ ] = unit
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/