search

logiccomp / lsl

4 stars 2 forks source link

Check-contract on trees? #11

Closed dbp closed 9 months ago

dbp commented 9 months ago

The following:

(define-struct leaf [value])
(define-struct node [left right])
(define-contract (Tree X) (OneOf (Leaf X) (Node (Tree X) (Tree X))))

(: height (-> (Tree Integer) Natural))
(define (height t)
  (cond [(leaf? t) 0]
        [(node? t) (add1 (max (height (node-left t)) (height (node-right t))))]))
(check-expect (height (make-leaf 0)) 0)
(check-expect (height (make-node (make-leaf 0) (make-node (make-leaf 0) (make-leaf 0)))) 2)

Works.

But this:

(check-contract height)

Errors.