using `@[to_dual]` more

Stream: PR reviews

[Kim Morrison]

            ┌── #35210
  #35208 ── #35209 ──┐
    │                #35213 ── #35214
    ├──── #35211 ────┘
    └──── #35215

[Kim Morrison]

#35208 is merged already!

[Kim Morrison]

So now ready for review we have:

[Kim Morrison]

chore: use @[to_dual] extensively in CompleteLattice #35209

[Kim Morrison]

chore: use @[to_dual] in Bounds/Image #35211

[Kim Morrison]

chore: use @[to_dual] in FixedPoints #35215

[Violeta Hernández]

Could you please merge master? The diff is bloated somewhat by the merged PRs.

[Eric Wieser]

Do we have an easy way of telling whether to_dual is actually generating the same lemmas?

[Violeta Hernández]

left reviews on all three

[Michael Rothgang]

Eric Wieser said:

Do we have an easy way of telling whether to_dual is actually generating the same lemmas?

You can use to_dual? to view the generated declaration (similarly to to_additive?).

[Jovan Gerbscheid]

You can also see the generated lemma by hovering over the attribute.

[Kim Morrison]

Violeta Hernández said:

Could you please merge master? The diff is bloated somewhat by the merged PRs.

Done.

[Kim Morrison]

Violeta Hernández said:

left reviews on all three

Thanks, I have dealt with the review comments on #35211 and #35215, and these are ready for review/merge again.

[Violeta Hernández]

I don't think the problems with #35211 have been adressed yet. to_dual doesn't automatically dualize docstrings, so you have to add them manually.

[Violeta Hernández]

#35215 LGTM :slight_smile:

[Kim Morrison]

Violeta Hernández said:

I don't think the problems with #35211 have been adressed yet. to_dual doesn't automatically dualize docstrings, so you have to add them manually.

Done now!

[Violeta Hernández]

I think your AI is misunderstanding the request... I don't want to add docstrings to every lemma tagged with to_dual, but rather, for any lemma where the dual had a docstring, you should add said docstring inside the to_dual tag.

[Kim Morrison]

I thought I did that!

[Kim Morrison]

Checking again, sorry.

[Kim Morrison]

Okay, I think I've corrected the doc-comments on all these PRs.