[Agda] Using functions before its declaration

[Amila Jayasekara]

Hi All,

I am new to Agda. I am running through code samples in "Power of Pi" [2]
paper.

While trying to type check following piece of code I get error in [1].

data Format : Set where


    Bad : Format


    End : Format


    Base : U → Format


    Plus : Format → Format → Format


    Skip : Format → Format → Format


    Read : (f : Format) → (⟦ f ⟧ → Format) → Format

⟦_⟧ : Format → Set


  ⟦ Bad ⟧ = Empty


  ⟦ End ⟧ = Unit


  ⟦ Base u ⟧ = el u


  ⟦ Plus f1 f2 ⟧ = Either ⟦ f1 ⟧ ⟦ f2 ⟧


  ⟦ Skip _ f ⟧ = ⟦ f ⟧


  ⟦ Read f1 f2 ⟧ = Sigma ⟦ f1 ⟧ (λ x → ⟦ f2 x ⟧)

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 ?

Feedback appreciated.

Thanks
Thejaka Amila

[1]
Not in scope:


  ⟦


  at /Users/thejaka/agda/ddl.agda:84,28-29

when scope checking ⟦

[2] http://dl.acm.org/citation.cfm?doid=1411203.1411213
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130419/1196c642/attachment.html