[Agda] Path to success with Agda?

Miëtek Bak mietek at bak.io
Tue Aug 30 10:29:47 CEST 2022

> 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.


More information about the Agda mailing list