diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-15 22:16:32 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-15 22:18:10 +0900 |
| commit | 8974e4b43e59ab7fadc803009cc9dff9d283f36d (patch) | |
| tree | c77a764804a7fc0f6ef3494c312b59edd5acc4df /huffman-encode.lisp | |
| parent | 05bb99b8f3f4f31699b945a01537f18e40f61bd8 (diff) | |
huffman-encode: rationalp-0-count-and-remove: Use `mv-nth` function.
Diffstat (limited to 'huffman-encode.lisp')
| -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))) |