[Agda] 2 tips for my fellow Agda newbies

[David Banas]

1. Always using extended lambda syntax (i.e. - \{ ...  -> ... }) seems to
make the Emacs mode interactive goal solving assistant more capable.

2. `C-c C-c` works not only for case expansion, but also for single term
expansion. For instance, it will expand "\{ x -> ... }" to "\{ < foo , bar
> -> ...}", when appropriate (i.e. - when x is an existential or product).
(Very helpful when first learning existentials.)

-db
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200826/9efe4a34/attachment.html>