[Agda] Re: C-style macros in Agda :)

[Dmytro Starosud]

Yes, I tried 'syntax', but for me it is not obvious enough how it should be
used.
What did you mean "Default arguments or eta-expansion for the propositional
equality"?
I am newbie in this area and I may not know enough about some features.
Could you point me to some related documents?

Thanks a lot,
Dmytro

2013/2/3 Andreas Abel <andreas.abel at ifi.lmu.de>

> Well you can always use the C preprocessor, but then you are restricted to
> batch-mode Agda.  Which isn't what you want, I suppose.
>
> Did you try the 'syntax' facility?   (Might not work...)
>
> Default arguments or eta-expansion for the propositional equality might
> help you, but these are not or not yet in Agda.
>
> Cheers,
> Andreas
>
>
> On 02.02.13 11:51 AM, Dmytro Starosud wrote:
>
>> I might be not clear enough.
>> Could you please refer to this
>> (https://github.com/dima-**starosud/Uniqueness-typing-in-**
>> Agda/blob/master/**HandleAPITest.agda<https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/HandleAPITest.agda>
>> ).
>> I want to get rid of:
>>
>> ⇒⟦ refl ⟧⇒
>>
>> e.g. replace it with "then", which would mean semicolon just like in
>> imperative program
>>
>> Best regards,
>> Dmytro
>>
>> 2013/2/1 Dmytro Starosud <d.starosud at gmail.com
>> <mailto:d.starosud at gmail.com>>
>>
>>
>>     Hello list,
>>
>>     I have the following code (simplified).
>>
>>     A B : Set
>>
>>     Ty : Set → Set → Set
>>     op : Set → Set
>>
>>     f : ∀ {A B} → op A ≡ op B → Ty A B → Ty B A
>>     x : Ty A B
>>
>>     y = f refl x
>>
>>     I should always write "f refl", because A and B is known at compile
>>     time and if "op A ≡ op B" is inhabited then "refl" is enough, I mean
>>     I don't need to write complex proof.
>>     But "op B : Set" is undecidable, so I cannot make that proof
>>     implicit, and also I cannot make it inferable (Agda not always wants
>>     to infer "refl" even if "op A" is exactly the same as "op B").
>>
>>     Is there any way to substitute "f refl" with some "g"? I mean
>>     something like C-style macros:
>>     #define g (f refl)
>>
>>     Thanks in advance,
>>     Dmytro
>>
>>
>>
>>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130203/4077f4b8/attachment.html