(module posn (file "../language/teachpack-dracula.scm")
#|
  (require (lib "unit.ss"))
  (require "defstructure.scm")
  (define-values/invoke-unit/infer defstructure@)
  ;(provide make-posn posn? posn-x posn-y)
  (defstructure posn
    (x (:assert (acl2-numberp x)))
    (y (:assert (acl2-numberp y))))
  ;(defun make-posn (x y) (posn x y))
  ;(defun posn? (x) (posn-p x))
  |#
  )