character-encoding-test

(in-package "ACL2")

(defun test-2 nil "ó")

(defthm len-test-2
  (equal (length (test-2)) 2)
  :rule-classes nil)