(module defthm mzscheme

  (require "../define-below/define-below.ss")

  (provide defthm defthm/local defaxiom)
  
  (define-syntax (defthm/local stx)
    (syntax-case stx ()
      [(_ name body hints ...)
       (if #f ;(definition-exists? #'name)
           #'(begin)
           #'(define-below name 
               (if #f
                   ;; 4-Oct-2006: 
                   ;; syntax checking seems to have gotten smarter in the module language.
                   ;; It flags the implicitly universally quantified vars as errors before running.
                   (void) ;(list body hints ...)
                   '(theorem: body))))]))
       
  (define-syntax (defthm stx)
    (syntax-case stx ()
      [(_ name body hints ...)
       (with-syntax ([provide-form (if #f ;(eq? (syntax-local-context) 'module)
                                       17 ; #`(provide (rename name #,(prefix #'name)))
                                       #'(begin))])
         #'(begin (defthm/local name body hints ...)
                  provide-form))]))

  ;; To a runtime system, defthm and defaxiom are the same no-op.
  (define-syntax (defaxiom stx)
    (syntax-case stx ()
      [(_ name body hints ...) (syntax/loc stx (defthm name body hints ...))]))
  )