<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">&lt;<a href="mailto:thejaka.amila@gmail.com" target="_blank">thejaka.amila@gmail.com</a>&gt;</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 &quot;Power of Pi&quot; [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 &quot;⟦_⟧&quot; is not defined for Format&#39;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>