lang/dracula-module-begin.ss
#lang scheme

(require (for-syntax "../proof/proof.ss" "../proof/syntax.ss"))

(provide dracula-module-begin)

(define-syntax (dracula-module-begin stx)
  (syntax-case stx ()
    [(_ form ...)
     (annotate-proof
      (make-proof
       (make-part
        'Dracula
        (syntax->loc stx)
        (map syntax->term (syntax->list #'(form ...)))))
      (with-syntax ([exports (datum->syntax stx `(,#'all-defined-out))])
        (syntax/loc stx
          (#%plain-module-begin
           (provide exports)
           form ...))))]))