The behavior is expected.
(I'm not sure it's a bug, probably just the efect of Arguments
that is local by default (maybe one can use the #[global]
attribute but I got used to put all the arguments at the end of sections))
Yes, I was wrong
@Enrico Tassi yes I should report because you were wrong to think it's an expected behaviour?
It is not a bug, it is a surprising behavior. Please don't report it.
I was surprised that implicits were recomputed even if no argument was added by section discharging. But this is not how the system works, it is really your directive which has a local scope. My bad.
Ok, let's go with it, but I hope that code will accept to work when put in ssralg, since that's the goal.
In any case, rewrite
worked!
Thanks all!
Julien Puydt has marked this topic as resolved.
Last updated: Jan 29 2023 at 16:02 UTC