Stream: math-comp devs

Topic: ✔ Ticket #928


view this post on Zulip Enrico Tassi (Sep 27 2022 at 14:03):

The behavior is expected.

view this post on Zulip 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))

view this post on Zulip Enrico Tassi (Sep 27 2022 at 14:04):

Yes, I was wrong

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Sep 27 2022 at 14:06):

It is not a bug, it is a surprising behavior. Please don't report it.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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