Jacques Carette
Jacques Carette
Right - `Agda.Builtin.Nat` is all in Agda, even though it says `Builtin`. The reason is that all `Agda.Builtin` are actually 'known' to Agda itself (for the purposes of reflection). It...
I don't think you're missing anything. This exact issue is why, with Bill Farmer and Michael Kohlhasse, we invented 'Realms'. Unfortunately these aren't implemented in Agda (just MMT).
As long as "forcing evaluation by `with`" and "forcing evaluation through pattern-matching" are 'the same computational behaviour', then yes. They sure have very different usability behaviour!!
Updated with an actual list.
The problem with local-only functions is that it's hard to prove things about them. Some of those helpers are independently useful, so those are 'easy', in a sense. For many...
> `initLast` is an early example of using views to write functions... for which the use of with is often (but not always) a corollary side-effect... so I'd be tempted...
Don't know if we could fill a book (yet), but certainly a non-trivial paper.
Actually, while I did start working on removing some uses of `with` that seemed like overkill, I specifically avoided `Data.List.Base` so as to not clash with #2355 . But then...
I've tried multiple things and: I can't definite `initLast` without using `with`. The `InitLast` view computes a lot, and that won't allow me to give any alternate definite (that I...
Agreed - did the first bit, no time right now to do the second.