Benedikt Ahrens
Benedikt Ahrens
> There is a lot of overlap with this code from |Foundations/PartA.v|: > > Could you take advantage of the existing code fruitfully? Regarding the last four maps (two of...
On 30/05/2019 21:30, Daniel R. Grayson wrote: > There is a lot of overlap with this code from |Foundations/PartA.v|: > > Could you take advantage of the existing code fruitfully?...
On 30/05/2019 22:13, Daniel R. Grayson wrote: > I just noticed my code can be simplified: It might be good to file a PR with these simplifications.
On 30/05/2019 21:30, Daniel R. Grayson wrote: > > Could you take advantage of the existing code fruitfully? I don't see how, but if you have a suggestion, I would...
On 02/06/2019 15:00, Daniel R. Grayson wrote: > On 30/05/2019 21:30, Daniel R. Grayson wrote: Could you take > advantage of the existing code fruitfully? > I don't see how,...
On 02/06/2019 16:13, Daniel R. Grayson wrote: > Isn't my proof also using the encode-decode method? > > Why should encode-decode proofs go into SyntheticHomotopyTheory? Because the same recipe can...
- One reason for treating MacOS and Linux differently is that Linux distribs come with a predefined way of obtaining ocaml, whereas MacOS does not. - There are no reasons...
> Regarding the de-duplication advantage — I agree with that. But surely that is an argument for changing our recommended build workflow on all OSes, not just Mac OS? Presumably...
On 18/12/2018 02:15, Daniel R. Grayson wrote: > The files in the package |Tactics| are unused. Can we remove them? I would prefer keeping them as long as they don't...
On 18/12/2018 19:30, Daniel R. Grayson wrote: > Well, okay, but what if we move them into other packages? They don't > warrant a separate package. Sure! Which package would...