val color_of: t:rbtree' -> Tot color
val color_of: t:rbtree' -> Tot color
let color_of t = match t with
  | E -> B
  | T c _ _ _ -> c
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module RBTree

(*
 * Red black trees, and verification of Okasaki's insertion algorithm
 * (https://wiki.rice.edu/confluence/download/attachments/2761212/Okasaki-Red-Black.pdf)
 *)

(* CH: how does this compare to Andrew Appel's verified RB-trees?
   http://www.cs.princeton.edu/~appel/papers/redblack.pdf
*)

(* color: Red or Black *)
type color =
  | R
  | B

(*
 * tree data type
 * either empty (E), or a node with a color, left child, key, and a right child
 *)
type rbtree' =
  | E
  | T: col:color -> left:rbtree' -> key:nat -> right:rbtree' -> rbtree'
/
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
RBTree.fst
t: RBTree.rbtree' -> RBTree.color
RBTree.rbtree' RBTree.B RBTree.color Prims.nat
let color_of t =
  
match t with
| E -> B
| T c _ _ _ -> c