#| Implements ACL2 keywords. |# (module acl2-top mzscheme (require (file "../define-below/define-below.ss")) (require-for-syntax "syntax-checks.scm") (provide acl2-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))])) )