[Agda] C-style macros in Agda :)

[Dmytro Starosud]

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/20130201/336e06c8/attachment.html