<div dir="ltr"><div><div>Hello Amila,<br><br>Maybe the problem is caused by indentation?<br></div>Please note definition and declaration must be at the same level.<br><br></div>Cheers,<br>Dmytro <br></div><div class="gmail_extra">
<br><br><div class="gmail_quote">2013/4/19 Amila Jayasekara <span dir="ltr"><<a href="mailto:thejaka.amila@gmail.com" target="_blank">thejaka.amila@gmail.com</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">Hi All,<div><br></div><div>I am new to Agda. I am running through code samples in "Power of Pi" [2] paper.</div><div><br></div><div>While trying to type check following piece of code I get error in [1].</div>
<div><br></div><div><div>data Format : Set where </div><div> Bad : Format </div>
<div> End : Format </div><div> Base : U → Format </div>
<div> Plus : Format → Format → Format </div><div> Skip : Format → Format → Format </div>
<div> Read : (f : Format) → (⟦ f ⟧ → Format) → Format </div><div><br></div><div><div>⟦_⟧ : Format → Set </div>
<div> ⟦ Bad ⟧ = Empty </div><div> ⟦ End ⟧ = Unit </div>
<div> ⟦ Base u ⟧ = el u </div><div> ⟦ Plus f1 f2 ⟧ = Either ⟦ f1 ⟧ ⟦ f2 ⟧ </div>
<div> ⟦ Skip _ f ⟧ = ⟦ f ⟧ </div><div> ⟦ Read f1 f2 ⟧ = Sigma ⟦ f1 ⟧ (λ x → ⟦ f2 x ⟧)</div>
</div><div><br></div><div>The error message is quite straight forward and says that "⟦_⟧" is not defined for Format's read operation. Does this mean that I cannot use and function before it is declared in the source file ?</div>
<div><br></div><div>Feedback appreciated.</div><div><br></div><div>Thanks</div><div>Thejaka Amila</div><div><br></div><div>[1] </div><div><div>Not in scope: </div>
<div> ⟦ </div><div> at /Users/thejaka/agda/ddl.agda:84,28-29 </div>
<div>when scope checking ⟦</div></div><div><br></div><div>[2] <a href="http://dl.acm.org/citation.cfm?doid=1411203.1411213" target="_blank">http://dl.acm.org/citation.cfm?doid=1411203.1411213</a></div></div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>