[Agda] Using functions before its declaration

[Dmytro Starosud]

Hello Amila,

Maybe the problem is caused by indentation?
Please note definition and declaration must be at the same level.

Cheers,
Dmytro


2013/4/19 Amila Jayasekara <thejaka.amila at gmail.com>

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130419/81827699/attachment.html