You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Here you would want to just write solve R' for ?, but since all the variables are in the context at this goal, what you have to do instead is to use the ring solver to get a path
This is mostly solved by #585. More precisely, the feature as requested above works, if the variables for the ring solver are introduced after all other variables. The remaining problem requires more work with deBrujin indices and I won't work on it any time soon.
I often find myself in the situation where I want to use the ring solver for parts of a long argument like this:
Here you would want to just write
solve R'
for ?, but since all the variables are in the context at this goal, what you have to do instead is to use the ring solver to get a pathand then fill the goal with
eq2 r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s
. This example can be found in the library at:https://github.com/agda/cubical/blob/master/Cubical/Algebra/CommRing/Localisation/Base.agda#L141
It would great if the ring solver could work with arguments from the context and it would save us quite a bit of boiler-plate code.
The text was updated successfully, but these errors were encountered: