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? _________________________ Racket Developers list: http://lists.racket-lang.org/dev
