Alex Gryzlov
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...