Zulip Chat Archive
Stream: maths
Topic: diamond for `rat.encodable`
Yury G. Kudryashov (Jul 12 2022 at 19:52):
The following fails:
import data.rat.denumerable
example : denumerable.to_encodable = rat.encodable := rfl
Last updated: May 02 2025 at 03:31 UTC