# Re: [racket-users] Apropos contracts: simple predicates and switching on and off

```Please read

The Contract Guide at
https://docs.racket-lang.org/guide/contracts.html?q=contracts```
```
It has many examples and gradually builds intuition. The ideal PR would be to
specific chapters there.

> On May 4, 2017, at 12:38 AM, Daniel Prager <daniel.a.pra...@gmail.com> wrote:
>
> Using Ben's left-pad example as a model I get the following re-write of the
> real-sqrt contract
>
>   (([x real?])
>    #:pre/name (x)
>    "non-negative argument expected"
>    (>= x 0)
>    . ->i .
>    [result (x) real?]
>    #:post/name (x result)
>    "the sqrt of zero is zero"
>    (implies (= x 0) (= result 0))
>    #:post/name (x result)
>    "the sqrt of a positive number is positive"
>    (implies (> x 0) (> result 0))
>    #:post/name (x result)
>    "result * result = x (to within error)"
>    (implies (> x 0) (<= (abs (- x (* result result))) 0.00000001)))
>
> Other than a bit of repetition — multiple uses of #:post/name — this is
> pretty darn close to what I was after.
>
> Like most people, when faced with something complex and a bit daunting — in
> this case the ->i contract combinator — I benefit from concrete examples.
>
> If enough people encourage me to "make a pull request" once I'm more familiar
> I'll propose some more examples myself.
>
> * * *
>
> My off-hand proposal would be to permit a variation on #:pre/name,
> #:post/name and friends to allow multiple clauses. For example:
>
>  #:post/name (x result)
>    ["sqrt of zero is zero" (implies (= x 0) (= result 0))]
>    ["sqrt of a positive number is positive" (implies (> x 0) (> result 0))]
>    ["result * result = x (to within error)"
>     (implies (> x 0) (<= (abs (- x (* result result))) 0.00000001))]
>
>
> Next stop ... boundaries.
>
>
> Thanks again
>
> Dan
>
>
> On Wed, May 3, 2017 at 1:57 PM, Ben Greenman <benjaminlgreen...@gmail.com>
> wrote:
>
> 1. To practice with dependent contracts, I made a "full" spec for the
>
> The exercise was fun, I learned a lot, and I think my solution is "as
> readable as possible" :) .
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an