<div dir="ltr">Hi All,<div><br></div><div style>I am new to Agda. I am running through code samples in "Power of Pi" [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 "⟦_⟧" 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 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>