# Zulip Chat Archive

## Stream: general

### Topic: to_additive & parallelism

#### Reid Barton (Sep 08 2020 at 12:23):

Just curious: Do we know how `to_additive`

interacts with proving lemmas in side tasks?

Since `to_additive`

translates definiitons to definitions and lemmas to lemmas, it should be possible for it to translate the statement of a lemma on the main task while translating the proof on a side task (which will join on the task that is checking the original lemma when it tries to fetch the original proof). But it would be easy to implement `to_additive`

in a way for which that doesn't happen, which would mean that the main task ends up joining on the checking the original proof, which wouldn't happen in the absence of `to_additive`

.

#### Reid Barton (Sep 08 2020 at 12:23):

Maybe it doesn't really matter because the theorems to which we apply `to_additive`

generally have trivial proofs.

#### Mario Carneiro (Sep 08 2020 at 12:27):

it does exactly what you fear

#### Mario Carneiro (Sep 08 2020 at 12:27):

it joins the proof on the main task

#### Mario Carneiro (Sep 08 2020 at 12:28):

you know, I'm apparently the sole author of `tactic.transform_decl`

but I don't recognize any of the functions in it

Last updated: Dec 20 2023 at 11:08 UTC