[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,
Dmytro
-------------- 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