[Agda] Using functions before its declaration

[Guillaume Brunerie]

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
>