fact: Fixpoint gen_bst (s : nat) (lo hi : nat) : G Tree := match s with | O => ret Leaf | S s' => freq [(1, ret Leaf) ;(if hi - lo < 2? then 0 else s, x <- choose (lo+1, hi-1);; l <- gen_bst s' lo x;; r <- gen_bst s' x hi;; ret (Node x l r))] end.
imports: QuickChick(QuickChick) List String ExtLib(Monad)