#| Provides read and read-syntax so that we can use #reader(lib "acl2-reader.scm" "acl2" "private")(module ...) to write ACL2 modules. (Teachpacks in particular use this.) |# (module acl2-reader mzscheme (require (file "acl2-readtable.scm")) (provide (rename my-read-syntax read-syntax) (rename my-read read)) (define (my-read . args) (parameterize ([current-readtable acl2-readtable]) (apply read args))) (define (my-read-syntax . args) (parameterize ([current-readtable acl2-readtable]) (apply read-syntax args))) )