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

[Dmytro Starosud]

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
).
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>

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130202/163702a2/attachment.html