PR #5487: feat(tactic/to_additive): Allow to_additive aft...

Stream: triage

[Random Issue Bot]

Today I chose PR 5487 for discussion!

feat(tactic/to_additive): Allow to_additive after norm_cast or continuity
Created by @Alex J Best (@alexjbest) on 2020-12-23
Labels: awaiting-author, merge-conflict, meta

Is this PR still relevant? Any recent updates? Anyone making progress?