(module defconst mzscheme
  (require-for-syntax "syntax-checks.ss")
  (require "../private/define-below.ss"
           "acl2-app.ss")
  (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))
         (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))
                    (quasisyntax/loc ref (acl2-expr the-const)))
                  (rename-below [the-ref name]))))]))

  )