val height (#a: eqtype) (#b: Type) (t: tree a b) : nat
let height (#a:eqtype) (#b:Type) (t:tree a b) : nat =
  match t with
  | Empty -> 0
  | Node _ _ h _ _ -> h
val height (#a: eqtype) (#b: Type) (t: tree a b) : nat
let height (#a: eqtype) (#b: Type) (t: tree a b) : nat =
match t with
| Empty -> 0
| Node _ _ h _ _ -> h
Vale.Lib.MapTree.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Lib.MapTree.fst
Prims.eqtype Vale.Lib.MapTree.tree Prims.nat
module Vale.Lib.MapTree
open FStar.Mul

(** Balanced tree implementation *)

type tree (a:eqtype) (b:Type) =
  | Empty : tree a b
  | Node : a -> b -> nat -> tree a b -> tree a b -> tree a b
val height (#a: eqtype) (#b: Type) (t: tree a b) : nat
t: Vale.Lib.MapTree.tree a b -> Prims.nat