[Agda] Path to success with Agda?

[Thorsten Altenkirch]

Maybe somebody should implement the smart case…

http://www.cs.nott.ac.uk/~psztxa/talks/shonan11.pdf

From: Agda <agda-bounces at lists.chalmers.se> on behalf of Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
Date: Tuesday, 30 August 2022 at 10:48
To: agda at lists.chalmers.se <agda at lists.chalmers.se>, Miëtek Bak <mietek at bak.io>
Subject: Re: [Agda] Path to success with Agda?


> On 30 Aug 2022, at 09:29, Miëtek Bak <mietek at bak.io> wrote:
>
>> On 30 Aug 2022, at 09:58, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
>>
>> So I wanted to mention the humble “case” expression, which functional programmers can more easily relate to, maybe. It’s less powerful that “with”, but sometimes works (wrt the not typechecking thing) when “with” won’t.
>
> It would be interesting to see an example in which `case` works and `with` does not.

I have some and will try to extract them from their context when I get a mo. However, I should qualify what I said:

  "but sometimes [case] works (wrt the not typechecking thing) when “with” won’t”

What I really meant was that, at the time, it was easier for me to use a “case" expression than to figure out how to still use “with” by moving lemmas to the top level, generalizing arguments a bit more, etc, etc. I expect there’s always a way with “with”.

And if you are heavily in to using “rewrite” (“with” disguised), then I guess “case” is not helpful.

Andy

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220831/3e338f10/attachment.html>