Notes on Ordmap.Ordnode

Stream: mathlib4

[Arien Malec]

(should this be OrdMap/OrdNode)?

I fixed a bunch of red here, including major surgery to repr to address the changes to Repr in Lean 4.

It's broken with failed to elaborate eliminator, expected type is not availableonrecOn uses, for which I understand there's a fix involving implicits and motives, but I don't follow the various Zulip discussions. There's also a very odd issue with ofList':

IR check failed at 'Ordnode.ofList'._rarg', error: unknown declaration 'List.decidableChain'

[Arien Malec]

I'm not at all sure if Ordnode works after all the fixes; when I try to test

#eval {1, 2, 3, 4, 5}: Ordnode

I get a typeclass instance problem.

[Mario Carneiro]

there should be parens?

[Mario Carneiro]

the typeclass instance problem would be a missing Insert instance. I'm not sure that was ever made to work

[Moritz Firsching]

link for convenience: mathlib4#1455

[Arien Malec]

Sigh, my ability to put a PR link in correctly is…poor.

[Arien Malec]

#eval ({1, 2, 3, 4, 5}: Ordnode ℕ)
(((∅ 1 ∅) 2 (∅ 3 ∅)) 4 (∅ 5 ∅))

[Mario Carneiro]

that looks like it's working