Tony Beta Lambda

YouTube is what I have in mind. But a play/pause functionality from keyboard would be convenient on all occasions :)

I guess it has to do with rust's requirements on the `Any` trait. For those who encountered the same problem: `std::mem::transmute` can be used to circumvent this, but is "the...

As a side note, Algebra/Monoids_and_Groups.v did not define a type for group morphisms; instead it just develops properties of monoid morphisms between groups. Also the fact that such morphisms preserve...

> * I believe that coercion is just custom subtyping rules. Am I right? We might need a more precise definition of "subtyping." For now, I would define coercion as...

This is totally fine, and that's the reason why we have named coercions, similar to the situation for typeclasses.

Like rust's `Into`?

And why we need named coercion instances: https://github.com/coq/coq/issues/9275 So another reason for making coercion typeclasses again.

Proposal: don't auto-insert `coerce` and leave everything to the library. Rationale: 1. Then coercion is totally a library-level thing. So one less language feature (which seems ad-hoc anyway) 2. Implicit...

> This way we make our language a bit less like a dynamic one. Making it look like a dynamic one is not part of our design goal if I...

> > Making it look like a dynamic one is not part of our design goal if I recall correctly. > > Yeah, [explicit is better than implicit](https://github.com/ice1000/mzi/blob/main/docs/design-choices.md#notation-lives-matter). But you...