[Agda] Path to success with Agda?

[Andreas Nuyts]

Hi,

I've been thinking along the lines of this smart case proposal when 
wondering about the possibility of judgemental naturality (w.r.t. the 
motive) of eliminators.

I think you have to be more careful when merging constraint sets: what 
if a new constraint n = b is added to a constraint set containing n' = 
b' where n' is blocked by the neutral subterm n? This situation doesn't 
seem to be addressed in the slides as they are.

Best,
Andreas N

On 31.08.22 14:57, Thorsten Altenkirch wrote:
>
> 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.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220901/feec39ca/attachment.html>