dolio

Not off hand. Does it still happen sometimes?

Never mind. I do see the problem. In the tests, `checkBytesMI` and `checkBytesMM` are wrong. The recursive call is: ``` checkBytesMI src larr rarr (l - 1) ``` But `l`...

Pushed an update to those functions.

I don't recall the exact details but [Henning Basold's thesis](https://liacs.leidenuniv.nl/~basoldh/thesis/) also tries to give a better account of mixed induction and coinduction, and it might have more general categorical semantics....

BTW, this is inconsistent with cubical: ```agda open import Cubical.Foundations.Prelude open import Cubical.Data.Bool open import Cubical.Data.Empty open import Cubical.Data.Unit open import Cubical.Relation.Nullary variable A B : Type record TSquash (A...

I'm not sure that's good enough due to #6359. E.G. you can do this: ```agda open import Cubical.Foundations.Prelude open import Cubical.Data.Bool open import Cubical.Data.Empty open import Cubical.Relation.Nullary variable A B...

My understanding is that the proposal is only to restrict definitions like: ```agda .foo : ... foo = ... ``` where `foo` itself is irrelevant. *Not* every definition that has...

I'm also for no instance at this point. If you think the existing instance is bad, it's better for no instance to exist, so that you get an error if...

So, I looked at this. A possible issue is that I see no way to implement a safe `fill` that doesn't do a lot of bounds checking. It just takes...

Hmm... It's been on my todo list for far too long to expose the constructors of various vector types. However, I hadn't thought of making an abstraction for it. I...