issue !4#660: `to_additive` unable to translate `toOneHom...

Stream: triage

[Random Issue Bot]

Today I chose issue 660 for discussion!

to_additive unable to translate toOneHomClass
Created by @Winston Yin (@winstonyin) on 2022-11-20
Labels:

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

[Michael Rothgang]

There has been lean#5770 proposed to address the core RFC lean4#1881. If I understood correctly, this should fix mathlib4#660.