<div dir="ltr">Hi All,<div><br></div><div style>I am new to Agda. I am running through code samples in &quot;Power of Pi&quot; [2] paper.</div><div style><br></div><div style>While trying to type check following piece of code I get error in [1].</div>
<div style><br></div><div style><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 style>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 style>Feedback appreciated.</div><div style><br></div><div style>Thanks</div><div style>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">http://dl.acm.org/citation.cfm?doid=1411203.1411213</a></div></div></div>