anchor.diff:                  let root, r' = AvlTree.DeleteMin r
                   AvlTree.Join (comparer, l, r', root)
   
  -    /// Internal. Only for use with [<StructuredFormatDisplay>].
  -    member private this.DisplayFormatted
  -        with get () = AvlTree.ToCodeString this
  -
       /// Prints a tree as F# code which, when executed, will re-create the tree.
       static member internal ToCodeString (tree : AvlTree<'T>) : string =
           /// Holds the printed code.
  
positive.code:             the AVL tree extracted from Isabelle/HOL, then specialized for the 'char' type. *)
  
  /// AVL Tree.
  [<NoEquality; NoComparison>]
  [<StructuredFormatDisplay("{DisplayFormatted}")>]
  [<DebuggerTypeProxy(typedefof<AvlTreeDebuggerProxy<int>>)>]
  //[<CompilationRepresentation(CompilationRepresentationFlags.UseNullAsTrueValue)>]
  type internal AvlTree<'T when 'T : comparison> =
      /// Empty tree.
      | Empty
  
negative.code:         | [], [] -> 0
          | [], _ -> -1
          | _, [] -> 1
  
          | Empty :: t1, Empty :: t2 ->
              AvlTree.CompareStacks (comparer, t1, t2)
  
          | Node (Empty, Empty, n1k, _) :: t1, Node (Empty, Empty, n2k, _) :: t2 ->
              match comparer.Compare (n1k, n2k) with
              | 0 ->
                  AvlTree.CompareStacks (comparer, t1, t2)
              | c -> c
  
          | Node (Empty, Empty, n1k, _) :: t1, Node (Empty, n2r, n2k, _) :: t2 ->
              match comparer.Compare (n1k, n2k) with
              | 0 ->
                  AvlTree.CompareStacks (comparer, Empty :: t1, n2r :: t2)
              | c -> c
  
          | Node (Empty, n1r, n1k, _) :: t1, Node (Empty, Empty, n2k, _) :: t2 ->
              match comparer.Compare (n1k, n2k) with
              | 0 ->
                  AvlTree.CompareStacks (comparer, n1r :: t1, Empty :: t2)
              | c -> c
  
          | Node (Empty, n1r, n1k, _) :: t1, Node (Empty, n2r, n2k, _) :: t2 ->
              match comparer.Compare (n1k, n2k) with
              | 0 ->
                  AvlTree.CompareStacks (comparer, n1r :: t1, n2r :: t2)
              | c -> c
  
          | Node (Empty, Empty, _, _) :: _, _ ->
              AvlTree.CompareStacks (comparer, Empty :: l1, l2)
          
          | Node (n1l, n1r, n1k, _) :: t1, _ ->
              AvlTree.CompareStacks (comparer, n1l :: Node (Empty, n1r, n1k, 0u) :: t1, l2)
          
          | _, Node (Empty, Empty, _, _) :: _ ->
              AvlTree.CompareStacks (comparer, l1, Empty :: l2)
          
          | _, Node (n2l, n2r, n2k, _) :: t2 ->
              AvlTree.CompareStacks (comparer, l1, n2l :: Node (Empty, n2r, n2k, 0u) :: t2)
                  
      //
  