<div dir="ltr">Dear <span style="font-size:13.333333969116211px;font-family:arial,sans-serif">Guillaume and </span><span style="font-size:13.333333969116211px;font-family:arial,sans-serif">Dmytro,</span><div><span style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br>
</span></div><div><span style="font-family:arial,sans-serif;font-size:13.333333969116211px">Thanks a lot for responses. </span><span style="font-family:arial,sans-serif;font-size:13.333333969116211px"> </span></div><div><span style="font-family:arial,sans-serif;font-size:13.333333969116211px">First writing </span><span style="font-family:arial,sans-serif;font-size:13.333333969116211px">type annotations, and then doing definition, fix the problem.</span></div>
<div><span style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></span></div><div><span style="font-family:arial,sans-serif;font-size:13.333333969116211px">Regards,</span></div><div><span style="font-family:arial,sans-serif;font-size:13.333333969116211px">Thejaka Amila</span></div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Apr 19, 2013 at 2:03 AM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Amila, for mutual inductive definitions, you should first write<br>
the typing annotations, and then the definitions.<br>
The following should work:<br>
<br>
<br>
data Format : Set<br>
⟦_⟧ : Format → Set<br>
<br>
data Format where<br>
<div class="im"> Bad : Format<br>
End : Format<br>
Base : U → Format<br>
Plus : Format → Format → Format<br>
Skip : Format → Format → Format<br>
Read : (f : Format) → (⟦ f ⟧ → Format) → Format<br>
<br>
</div><div class="im">⟦ Bad ⟧ = Empty<br>
⟦ End ⟧ = Unit<br>
⟦ Base u ⟧ = el u<br>
⟦ Plus f1 f2 ⟧ = Either ⟦ f1 ⟧ ⟦ f2 ⟧<br>
⟦ Skip _ f ⟧ = ⟦ f ⟧<br>
⟦ Read f1 f2 ⟧ = Sigma ⟦ f1 ⟧ (λ x → ⟦ f2 x ⟧)<br>
<br>
<br>
</div>(and Dmytro is right that something was wrong in your indentation)<br>
<br>
Cheers,<br>
Guillaume<br>
<br>
2013/4/19 Dmytro Starosud <<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>>:<br>
<div class="HOEnZb"><div class="h5">> Hello Amila,<br>
><br>
> Maybe the problem is caused by indentation?<br>
> Please note definition and declaration must be at the same level.<br>
><br>
> Cheers,<br>
> Dmytro<br>
><br>
><br>
> 2013/4/19 Amila Jayasekara <<a href="mailto:thejaka.amila@gmail.com">thejaka.amila@gmail.com</a>><br>
>><br>
>> Hi All,<br>
>><br>
>> I am new to Agda. I am running through code samples in "Power of Pi" [2]<br>
>> paper.<br>
>><br>
>> While trying to type check following piece of code I get error in [1].<br>
>><br>
>> data Format : Set where<br>
>> Bad : Format<br>
>> End : Format<br>
>> Base : U → Format<br>
>> Plus : Format → Format → Format<br>
>> Skip : Format → Format → Format<br>
>> Read : (f : Format) → (⟦ f ⟧ → Format) → Format<br>
>><br>
>> ⟦_⟧ : Format → Set<br>
>> ⟦ Bad ⟧ = Empty<br>
>> ⟦ End ⟧ = Unit<br>
>> ⟦ Base u ⟧ = el u<br>
>> ⟦ Plus f1 f2 ⟧ = Either ⟦ f1 ⟧ ⟦ f2 ⟧<br>
>> ⟦ Skip _ f ⟧ = ⟦ f ⟧<br>
>> ⟦ Read f1 f2 ⟧ = Sigma ⟦ f1 ⟧ (λ x → ⟦ f2 x ⟧)<br>
>><br>
>> The error message is quite straight forward and says that "⟦_⟧" is not<br>
>> defined for Format's read operation. Does this mean that I cannot use and<br>
>> function before it is declared in the source file ?<br>
>><br>
>> Feedback appreciated.<br>
>><br>
>> Thanks<br>
>> Thejaka Amila<br>
>><br>
>> [1]<br>
>> Not in scope:<br>
>> ⟦<br>
>> at /Users/thejaka/agda/ddl.agda:84,28-29<br>
>> when scope checking ⟦<br>
>><br>
>> [2] <a href="http://dl.acm.org/citation.cfm?doid=1411203.1411213" target="_blank">http://dl.acm.org/citation.cfm?doid=1411203.1411213</a><br>
>><br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>><br>
><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
</div></div></blockquote></div><br></div>