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

[Andreas Abel]

I do not know whether this is a bug in Agda, but MiniAgda accepts this  
one.

data Unit : Set { unit : Unit }

mutual {

   codata T : Set 1
   { intro : (t : T) -> bracket t -> T
   }

   fun bracket : T -> Set
   { bracket (intro t b) = Unit
   }

}

Cheers,
Andreas

On Sep 20, 2010, at 1:34 PM, David Leduc wrote:

>
> open import Coinduction
>
> data unit : Set where
>  * : unit
>
> mutual
>  data T : Set1 where
>    intro : (t : ∞ T) -> [ ♭ t ] -> T
>
>  [_] : T -> Set
>  [ intro _ _ ] = unit

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/