Jacques Carette
Jacques Carette
This seems like a bunch of different, non-trivial bugs. Do you want to have a stab at them, or do you want me to look first?
I agree that the "use theory refinement" project should happen first, then this.
There is no need to use `gravitionalAccelConst` verbatim. We could define our own. The problem with that is that if we re-use anything in our standard definitions that *do* rely...
If we came up with a design then... no.
Generally I agree. Though for the first example (removing import statements that are not needed), I would much prefer to do it the other way around: only include what is...
There is a lot of stuff going on here. Certainly I agree with everything said in the @smiths - @bmaclach exchange past the original analysis. As far the detailed results...
This ticket probably needs a very careful analysis - I'm guessing some parts should become a project and some should just be split into small issues.
Yes, what you've done is definitely a step in the right direction.
Ooh, this is fascinating. All my instincts say that, in the situation outlined in the commit message, it should be completely safe to inline. So I'm super-interested in understanding why...
@xekoukou you're mixing two things: Agda's verbosity (which is really not bad at all, but could be improved here and there) and the active choice of agda-unimath to choose very...