<br><div class="gmail_quote">On Tue, Sep 21, 2010 at 2:15 PM, David Leduc <span dir="ltr"><<a href="mailto:david.leduc6@googlemail.com">david.leduc6@googlemail.com</a>></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) -> (t : ∞ T) -> [ ♭ t ] -> T<br>
<br>
[_] : (t : T) -> Set<br>
[ makeT A _ _ ] = A<br>
<br>
t : T<br>
t = makeT unit (♯ t) tt<br></blockquote><div><br></div><div>It'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't look at the definition until you'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'). When checking the definition of tt', t has been checked already,</div><div>so you're allowed to look at its definition.</div><div><br></div><div>/ Ulf</div></div>