[Agda] C-style macros in Agda :)

Dmytro Starosud d.starosud at gmail.com
Fri Feb 1 22:35:50 CET 2013

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,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130201/336e06c8/attachment.html

More information about the Agda mailing list