Jacques Carette
Jacques Carette
I think I liked `OneMorphism` and `ZeroMorphism` (without the cuteness) more than `The`. In some ways, if these files are meant to be used qualified, then just `Morphism` might work,...
`Unique` has a certain charm to it, I agree.
It does make a lot of sense to seriously consider adding some such symbol - basically because 200 years of Group Theory has continued to do so. So they find...
I think `quasigroup` and `loop` use \\\\ and // .
I don't have a good suggestion, as I don't really know the actual effect the refactoring would have. It might range from harmless to completely unacceptable.
Such lemmas would definitely be guaranteed low-disruption. Thus definitely a viable path.
The tactic solvers make the dependency graph completely crazy. Simplicity for the developer does not always mean the same for the library as whole. Some tedious proofs are absolutely worth...
I agree with @Taneb . I think the issue is exactly the same as with Peano Nats and blocks-of-binary-digits: one is great for proofs, one is great for efficient computation....
I obviously agree emphatically with this. And, to a certain extent, this is roughly the work that Yasmine did for her Ph.D. thesis. If you couple it with the produce-documented-human-readable-code...
Of course: [Drasil](https://github.com/JacquesCarette/Drasil) . Under Papers/WellUnderstood is our most recent write-up. The [wiki](https://github.com/JacquesCarette/Drasil/wiki) also have a wealth of information.