[Agda] Using functions before its declaration

[Amila Jayasekara]

Dear Guillaume and Dmytro,

Thanks a lot for responses.
First writing type annotations, and then doing definition, fix the problem.

Regards,
Thejaka Amila


On Fri, Apr 19, 2013 at 2:03 AM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> Hello Amila, for mutual inductive definitions, you should first write
> the typing annotations, and then the definitions.
> The following should work:
>
>
> data Format : Set
> ⟦_⟧ : Format → Set
>
> data Format where
>     Bad : Format
>     End : Format
>     Base : U → Format
>     Plus : Format → Format → Format
>     Skip : Format → Format → Format
>     Read : (f : Format) → (⟦ f ⟧ → Format) → Format
>
> ⟦ 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 ⟧)
>
>
> (and Dmytro is right that something was wrong in your indentation)
>
> Cheers,
> Guillaume
>
> 2013/4/19 Dmytro Starosud <d.starosud at gmail.com>:
> > 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
> >>
> >
> >
> > _______________________________________________
> > 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/450bffe2/attachment.html