Enrico Tassi (Sep 27 2022 at 14:03): Enrico Tassi (Sep 27 2022 at 14:03):The behavior is expected.
Pierre Roux (Sep 27 2022 at 14:04):(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))
Enrico Tassi (Sep 27 2022 at 14:04):Yes, I was wrong
Julien Puydt (Sep 27 2022 at 14:06):@Enrico Tassi yes I should report because you were wrong to think it's an expected behaviour?
Enrico Tassi (Sep 27 2022 at 14:06):It is not a bug, it is a surprising behavior. Please don't report it.
Enrico Tassi (Sep 27 2022 at 14:08):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.
Julien Puydt (Sep 27 2022 at 14:13):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!
Notification Bot (Sep 27 2022 at 14:13):Julien Puydt has marked this topic as resolved.
Last updated: Jan 29 2023 at 16:02 UTC