<br><div class="gmail_quote">On Tue, Sep 21, 2010 at 2:15 PM, David Leduc <span dir="ltr">&lt;<a href="mailto:david.leduc6@googlemail.com">david.leduc6@googlemail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi,<br>
<br>
In the definition of  t  below, the type checker does not see that<br>
[ t ]  is equal to  unit  and thus raise an error.<br>
I believe it is a bug, isnt it?<br><br>
module test where<br>
<br>
open import Coinduction<br>
<br>
data unit : Set where<br>
  tt : unit<br>
<br>
mutual<br>
  data T : Set1 where<br>
    makeT : (A : Set) -&gt; (t : ∞ T) -&gt; [ ♭ t ] -&gt; T<br>
<br>
  [_] : (t : T) -&gt; Set<br>
  [ makeT A _ _ ] = A<br>
<br>
t : T<br>
t = makeT unit (♯ t) tt<br></blockquote><div><br></div><div>It&#39;s not a bug. In order to see that [ t ] is unit you need to know the definition of t</div><div>and you can&#39;t look at the definition until you&#39;ve type checked it. To make it work</div>
<div>you can do the following:</div><div><br></div><div><div>mutual</div><div>  t : T</div><div>  t = makeT unit (♯ t) tt′</div><div><br></div><div>  tt′ : [ t ]</div><div>  tt′ = tt</div></div><div><br></div><div>In this case the definition of t can be type checked (just knowing the type, but not</div>
<div>the definition of tt&#39;). When checking the definition of tt&#39;, t has been checked already,</div><div>so you&#39;re allowed to look at its definition.</div><div><br></div><div>/ Ulf</div></div>