Skip to content

Instantly share code, notes, and snippets.

#lang rosette
(require rackunit syntax/parse/define)
;; https://openai.com/blog/formal-math/
(define-simple-macro (prove e ...) (check-pred unsat? (verify (begin e ...))))
(test-case "Problem 1"
(define-symbolic* x p real?)
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.

Keybase proof

I hereby claim:

  • I am anishathalye on github.
  • I am anish (https://keybase.io/anish) on keybase.
  • I have a public key whose fingerprint is 72EE 4824 FA6E FF1F E750 A015 C3F6 E4F5 086B 3B32

To claim this, I am signing this object: