Zulip Chat Archive
Stream: Is there code for X?
Topic: dual
Scott Morrison (Jul 17 2023 at 09:04):
Where is
def dual (a : α) : αᵒᵈ := a
?
I am bemused to not be finding it right after the definition of OrderDual...
Eric Wieser (Jul 17 2023 at 09:08):
Eric Wieser (Jul 17 2023 at 09:08):
It's in a different file because Equiv isn't available yet
Eric Wieser (Jul 17 2023 at 09:08):
Or at least, at one point it wasn't
Last updated: Dec 20 2023 at 11:08 UTC