rbt.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. Style: centered; floating; windowed.

Module RBT := MSets.MSetRBT.Make Nat_as_OT.

Definition build_trees (leaves: list nat) :=
  List.fold_left (fun trs n =>
      RBT.add n (hd RBT.empty trs) :: trs)
    leaves [] |> List.rev.

Compute build_trees [1;2;3;4;5;6].= []: RBT.t |> list

Compute build_trees [2;1;4;3;6;5].= []: RBT.t |> list

Compute build_trees [6;5;4;1;2;3].= []: RBT.t |> list