Argh, I wanted the other way (negative). I always get the directions confused. Sorry.
On Jan 15, 2015, at 11:26 AM, David Van Horn <dvanh...@cs.umd.edu> wrote: > On 1/15/15, 11:17 AM, Matthias Felleisen wrote: >> >> >> On Jan 15, 2015, at 11:13 AM, David Van Horn <dvanh...@cs.umd.edu> >> wrote: >> >>> 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. >> >> >> My contract is stronger than yours. So why will it not go through? >> >> > > 100 is (>/c 0) but (f 100) divides by zero. > > David > _________________________ Racket Developers list: http://lists.racket-lang.org/dev
