(module defconst mzscheme
  (require-for-syntax "syntax-checks.scm"
                      "../modular/expansion/proof-syntax.scm")
  (require "../define-below/define-below.ss"
           "acl2-app.scm")
  (provide defconst)

  (define-syntax (defconst stx)
    (syntax-case stx ()
      [(_ name expr)
       (begin
         (unless (legal-constant-name? #'name)
           (raise-syntax-error
            #f
            "Constant names must begin and end with asterisks (*)."
            stx #'name))
         (make-event
          stx
          (syntax/loc stx
            (begin (define the-const expr)
                   (define-syntax (the-ref ref)
                     (unless (identifier? ref)
                       (raise-syntax-error
                        #f "invalid reference to defconst name" ref))
                     (make-expr (syntax/loc ref name)
                                (syntax/loc ref (acl2-expr the-const))))
                   (rename-below [the-ref name])))))]))

  )