diff options
| -rw-r--r-- | huffman-encode.lisp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp index 9cb44d5..febf07b 100644 --- a/huffman-encode.lisp +++ b/huffman-encode.lisp @@ -1,6 +1,8 @@ ;;; Provide Huffman encoding (in-package "ACL2") +(local (include-book "tools/mv-nth" :dir :system)) + ;;; Deine huffman tree (defun nodep (x) (declare (xargs :guard t)) @@ -321,7 +323,7 @@ (message-to-pairs rest))))) (defthm rationalp-0-count-and-remove - (rationalp (car (count-and-remove e x)))) + (rationalp (mv-nth 0 (count-and-remove e x)))) (defthm symbol-weight-pair-listp-message-to-pairs (symbol-weight-pair-listp (message-to-pairs x))) |