[Agda] syntax declaration
Martin Escardo
m.escardo at cs.bham.ac.uk
Mon Mar 23 18:19:40 CET 2020
Also you will need to write
syntax exists A P = ex x : A , P x
without the round brackets, I think.
Martin
On 23/03/2020 17:18, Martin Escardo wrote:
> Use a different colon (:) symbol, such as the one you get by typing \:4
> in emacs. I think the normal colon is reserved. Martin
>
> On 23/03/2020 16:53, michel.levy.imag at free.fr wrote:
>> I made the following statement
>>
>> data exists (A : Set)(P : A -> Set): Set where
>> <_,_> : (a : A) -> P a -> exists A P
>>
>> I would like to rewrite (exists A P) as, for example, (ex (x : A) P x).
>> But I don't understand how to do it. I tried :
>>
>> syntax exists A P = ex (x : A) , P x
>>
>> but I had the mistake : syntax must use holes exactly once
>>
>> Can you explain to me how to use the syntax declaration on this
>> example ? What are these holes in my syntax statement ?
>>
>
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
More information about the Agda
mailing list