[Agda] C-style macros in Agda :)

Dmytro Starosud d.starosud at gmail.com
Mon Feb 4 20:56:18 CET 2013

Do you mean something like this?



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

More information about the Agda mailing list