summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-15 22:16:32 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-15 22:18:10 +0900
commit8974e4b43e59ab7fadc803009cc9dff9d283f36d (patch)
treec77a764804a7fc0f6ef3494c312b59edd5acc4df
parent05bb99b8f3f4f31699b945a01537f18e40f61bd8 (diff)
huffman-encode: rationalp-0-count-and-remove: Use `mv-nth` function.
-rw-r--r--huffman-encode.lisp4
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)))