Jacques Carette
Jacques Carette
Wild guess (don't have time to look at the details right now): you have a different version of stdlib. 1.7 and 2.0 are very different, and agda-categories only works for...
You might be able to pull PR #452 into your development, and that might work. Or revert to 1.7.
Typo, yes. `git merge` the commits?
So can I close this issue?
Can't we use some kind of pair as `Index`, to index by more than one thing "at once"? [This is different than double-indexing].
I mean something that would mean the same as `a[i,j]`, i.e. `Index(a, Pair(i,j))` as an `Expr`. I don't know if we have the `Pair` constructor (or something like it) in...
I see, that is a rather different issue indeed. `QDefinition` really is for defining single values (depending on an arbitrary number of other things, which do not need to be...
As I revisit this: the correct fix is to add 'indexing' to `Expr`. It's a bit of a cheat, since indexing is really not very different from application (vectors, for...
Nope, unfortunately not. I'll push it up on my priority list.
Looking at this code again, I don't think this is quite the right approach -- it loses too much type information. I think the 'static' information should be tracked in...