John Lång

Wow, I even managed to define an infix arrow syntax `x ↦ M` corresponding with `λ x → M` constructing values of my Pi type!

It is remarkable how even function types aren't truly special in Agda

OK, that's true. Still, I'm quite surprised that I could define my own lambda abstraction equivalent, as well as the Pi type.

Actually, so far none of the hyperlinks seem to work for me, except for the top-level chapter headings in the contents.

Thanks for the link!

Changing the `Leaf`case return value to `undefined` fixes the error, but I feel like that's not the best way to solve this.

Ah, there seems to be a link to another chapter that supposedly helps to fix the problem with `delmin`. The link doesn't work for me, though.

Here's the link: https://privatebin.net/?2b64c18c8da919bc#BPts1wpxjXVxaLyzqM9RdhP5Zwtp6E2AqhkxcainToFg I haven't modified the signatures. My implementation for `insR` is pretty much the mirror image of `insL`. If I comment out everything about `insR`, then these...

I believe we need either this or https://git.ksfmedia.fi/taco/persona/-/merge_requests/357 for the credentials migration.

Apparently, things like lambda terms and infix notation with backticks don't work with refinement types. This example is quite contrived but I think it makes my point clear: The type...