pi3js2
pi3js2
So, interpolate in Cubical.Foundations.Interpolate, then? I can update the MR. (Or "interp"? It seems to occur in various computer math libraries...) It could just go in CartesianKanOps, even private. Or...
> Personally, I also find the ad-hoc interval expressions hard to read; there's not enough context to see at a glance what their _intent_ is. I think having descriptive names,...
Sorry! I have renamed the operator to `interpolateI`, and I also made it private and put it in CartesianKanOps.
@mortberg so sorry :facepalm: should be better now (`make build` got past these files locally at least...)
Attempted to fix the new CI problem, sorry again. I am trying to run `make check` locally but it seems to get stuck for a long time at `Cubical.Algebra.Group.GroupPath`, I...
Sorry... I shouldn't have tried to change things. I reverted to the previous approved state, and changed only the name "erp" to "interpolateI". I hope that's OK. :smile: Unfortunately I...
Attempted CI fix. I am praying that this PR can finally be over... I still haven't been able to run checks locally but I could try again soon.
> We changed it so that Foundations.Everything is automatically generated, so no need to edit it manually anymore Nice! Rebased. :pray: :pray:
Thanks, glad my eyeballs work :) Just for context: I was working on this example to try to run some closed computations. I got the computations working in Agda now,...