[Agda] C-style macros in Agda :)

[Dmytro Starosud]

Do you mean something like this?

http://publications.lib.chalmers.se/records/fulltext/146810.pdf
<http://publications.lib.chalmers.se/records/fulltext/146810.pdf,>

Thanks,
Dmytro


2013/2/4 Nils Anders Danielsson <nad at chalmers.se>

> On 2013-02-01 22:35, Dmytro Starosud wrote:
>
>> Is there any way to substitute "f refl" with some "g"?
>>
>
> One option, that may or may not work for you, is to switch from Set to a
> universe for which a conservative approximation of equality is
> decidable. Then you can use an implicit argument of type
>
>   True ("decision procedure says yes").
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130204/a96443f9/attachment.html