tree-insert

(datatype tree
  _______________________
  []: tree;

  Val: A; Left: tree; Right: tree;
  _______________________
  [Val Left Right]: tree;

  Left: tree, Right : tree >> P;
  _____________________________
  [Val Left Right]: tree >> P;)

(define insert-val
  {number --> tree --> tree}
  A []       -> [A [] []]
  A [V L R]  -> [V (insert-val A L) R] where (< A V)
  A [V L R]  -> [V L (insert-val A R)] where (> A V)
  )

(define smallest-val
  {tree --> number}
  [V () ()] -> V
  [V L R] -> (smallest-val L))

*\type error in rule 2 of insert-val \*