From 5163a157c4f9b552db220efaa753f210518817fe Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 9 Sep 2021 22:53:04 +0900 Subject: Add `(in-package "ACL2")` lines. --- L-99.lisp | 2 ++ binary-tree.lisp | 2 ++ combinations.lisp | 2 ++ consecutive-fibonacci-numbers-are-coprime.lisp | 3 ++- divisor-list.lisp | 1 + fast-expt.lisp | 2 ++ flist.lisp | 2 ++ list-monad.lisp | 1 + palindrome-sandwich.lisp | 1 + peano.lisp | 2 ++ permutations.lisp | 2 ++ pigeonhole.lisp | 2 ++ units.lisp | 2 ++ 13 files changed, 23 insertions(+), 1 deletion(-) diff --git a/L-99.lisp b/L-99.lisp index 3c8dc71..b1854fc 100644 --- a/L-99.lisp +++ b/L-99.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + ;; P01 (*) Find the last box of a list. (defun my-last (x) (declare (xargs :guard (and (true-listp x) diff --git a/binary-tree.lisp b/binary-tree.lisp index b26b8fb..aab189d 100644 --- a/binary-tree.lisp +++ b/binary-tree.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defun emptyp (x) (atom x)) diff --git a/combinations.lisp b/combinations.lisp index 93c3b67..9495676 100644 --- a/combinations.lisp +++ b/combinations.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defun cons-all (e x) (declare (xargs :guard (true-listp x))) (if (endp x) diff --git a/consecutive-fibonacci-numbers-are-coprime.lisp b/consecutive-fibonacci-numbers-are-coprime.lisp index af0a534..0146dc1 100644 --- a/consecutive-fibonacci-numbers-are-coprime.lisp +++ b/consecutive-fibonacci-numbers-are-coprime.lisp @@ -1,4 +1,5 @@ -;; consecutive-fibonacci-numbers-are-coprime.lisp: 隣り合うフィボナッチ数は互いに素である +;;; consecutive-fibonacci-numbers-are-coprime.lisp: 隣り合うフィボナッチ数は互いに素である +(in-package "ACL2") ;; 数字を足したり引いたりする関数に関する証明をするときに便利な Book (include-book "arithmetic/top-with-meta" :dir :system) diff --git a/divisor-list.lisp b/divisor-list.lisp index 21cbb10..20d2793 100644 --- a/divisor-list.lisp +++ b/divisor-list.lisp @@ -1,4 +1,5 @@ ;;; divisor-list.lisp: 約数に関する証明 +(in-package "ACL2") ;; e が x の約数であるかどうかを調べる述語 (defmacro divisorp (e x) diff --git a/fast-expt.lisp b/fast-expt.lisp index 3318946..d3fb779 100644 --- a/fast-expt.lisp +++ b/fast-expt.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defmacro square (x) `(* ,x ,x)) diff --git a/flist.lisp b/flist.lisp index dc6ffe7..8e38395 100644 --- a/flist.lisp +++ b/flist.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defun true-flistp (x) (if (endp x) (null x) diff --git a/list-monad.lisp b/list-monad.lisp index f7a6425..56a79dd 100644 --- a/list-monad.lisp +++ b/list-monad.lisp @@ -1,5 +1,6 @@ ;;; list-monad.lisp ;;; ACL2 でリストモナドがモナド則を満たしていることを示す +(in-package "ACL2") ;; ACL2 では第一級の関数は使えないため、値としての関数は連想リストで表現する ;; ACL2 には apply$ という限定的な高階関数を実現する機能があるがよく分かってい diff --git a/palindrome-sandwich.lisp b/palindrome-sandwich.lisp index 98f5e64..b2d2a9d 100644 --- a/palindrome-sandwich.lisp +++ b/palindrome-sandwich.lisp @@ -7,6 +7,7 @@ ;;; (true-listp y)) ;;; (equal (palindromep (app y (app x (rev y)))) ;;; (palindromep x)))) +(in-package "ACL2") ;; 二つのリストを連結する (defun app (x y) diff --git a/peano.lisp b/peano.lisp index 8fedc56..9ea24ba 100644 --- a/peano.lisp +++ b/peano.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defmacro zero? (x) `(equal ,x nil)) diff --git a/permutations.lisp b/permutations.lisp index d75a4d2..ef843ba 100644 --- a/permutations.lisp +++ b/permutations.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defun mapcar-cons (e x) (declare (xargs :guard (true-listp x))) (if (endp x) diff --git a/pigeonhole.lisp b/pigeonhole.lisp index 91c221f..23b8637 100644 --- a/pigeonhole.lisp +++ b/pigeonhole.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defun member-if-over-1 (x) (cond ((endp x) nil) ((< 1 (car x)) x) diff --git a/units.lisp b/units.lisp index 4b353e1..8533509 100644 --- a/units.lisp +++ b/units.lisp @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defun m (x) x) -- cgit v1.2.3