#| Implements ACL2 keywords. |# (module acl2-top mzscheme (require (file "../private/define-below.ss")) (require-for-syntax "syntax-checks.ss") (provide (rename acl2-top #%top)) (define-syntax (acl2-top stx) (syntax-case stx () [(_ . keyword) (keyword-syntax? #'keyword) (syntax/loc stx (#%datum . keyword))] [(_ . top) (syntax/loc stx (top/error . top))])) )