[Agda] rewrite keyword

Georgi Lyubenov godzbanebane at gmail.com
Mon Mar 30 21:59:38 CEST 2020


Hi!

\^l brings up the superscript 'l' as one of four choices for me - I can
choose which one I want by using the corresponding number
[image: 2020-03-30-225522_377x30_scrot.png]

Rewrite is described as being syntactic sugar for 'with' and 'with'
itself is not a term. What kind of term are you expecting out of the
'rewrite'?

=======
Georgi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200330/d8b048f3/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 2020-03-30-225522_377x30_scrot.png
Type: image/png
Size: 4470 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200330/d8b048f3/attachment.png>


More information about the Agda mailing list