#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 ...))))]))