Zulip Chat Archive
Stream: general
Topic: Complex number doesn't have has_repr
Yufan Lou (Feb 25 2020 at 03:04):
Today I had some discussions with schoolmates about complex numbers and I wanted to try to do some simple calculation with Lean, but when I did
#eval complex.mk 3 4
I got an error saying it doesn't have has_repr and got a complex internal structure dump instead
Reid Barton (Feb 25 2020 at 03:26):
Does real have one?
Last updated: May 02 2025 at 03:31 UTC