Alex Gryzlov

A few years ago, I've helped making a port of Coq's formalized binary arithmetic here: https://github.com/sbp/idris-bi. This includes both unbounded and bounded inductively defined binaries. The original Coq library is...

Yes, you can make a `List (BizMod2 8)` for a byte array. If you want a primitive byte type, there's https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Bits.idr, but you won't be able to prove anything about...

@zaoqi probably here: https://twitter.com/edwinbrady/status/1119675651181699072

I guess one way to do it would be to unify records and namespaces to some extent?

Yeah I think going for a simpler solution and assuming a fixed order might be good enough for a start. This is what happens when matching on auto implicits already...

Also this seems to overlap with the recent research of @gallais et al on [Frex](https://www.cl.cam.ac.uk/~jdy22/papers/frex-indexing-modulo-equations-with-free-extensions.pdf), though I'm not sure what stage (:wink:) that work is at.

Same here

+1 for ``

I think OTT/HoTT/CTT aren't so much about effects, but rather about exploring the nature of equality, allowing to do proofs on functions (`funext` is provable in those), codata, real numbers...

Here are a couple of recent CBPV-style systems for dependent effects: * https://arxiv.org/abs/1706.07997 Vakar, "In Search of Effectful Dependent Types" * https://arxiv.org/abs/1710.02594 Ahman, "Fibred Computational Effects" * https://github.com/danelahman/POPL18 partial Agda...