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: Dec 20 2023 at 11:08 UTC