Skip to content

Instantly share code, notes, and snippets.

@fogus
Created May 28, 2010 18:19
Show Gist options
  • Save fogus/417513 to your computer and use it in GitHub Desktop.
Save fogus/417513 to your computer and use it in GitHub Desktop.
(kontract doubler
[x]
:requires
(pos? x)
:ensures
(= (* 2 x) %)
[x y]
:requires
(pos? x)
(pos? y)
:ensures
(= (* 2 (+ x y)) %))
;;; OR OR OR
(contract doubler
[x]
(requires
(pos? x))
(ensures
(= (* 2 x) %))
[x y]
(requires
(pos? x)
(pos? y))
(ensures
(= (* 2 (+ x y)) %)))
@ordnungswidrig
Copy link

(kontract doubler
[x]
requires
  (pos? x)

ensures
  (= (* 2 x) %)

[x y]
requires
  (pos? x)
  (pos? y)
       
ensures
  (= (* 2 (+ x y)) %))

@citizen428
Copy link

I prefer the first one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment