On 1/15/15, 11:04 AM, Matthias Felleisen wrote: > > Well that got me all excited. So I tried to get the sample module > to pass the verification step -- until I realized how restricted > the grammar is! > > (module f racket (provide (contract-out [f (real? . -> . > integer?)])) (define (f n) (/ 1 (- 100 n)))) > > I would love to be able to use at least (and/c real? (>/c 0)) for > the domain so I can get the example done. > > Or am I overlooking a way to make this work here?
The >/c contract is there, but missing from the grammar (we'll fix that). But (>/c 0) will not make this program verify. You want this contract: ((and/c real? (lambda (x) (not (= x 100)))) . -> . real?) Using this contract, the program verifies. David _________________________ Racket Developers list: http://lists.racket-lang.org/dev
