diff options
| -rw-r--r-- | L-99.lisp | 2 | ||||
| -rw-r--r-- | binary-tree.lisp | 2 | ||||
| -rw-r--r-- | combinations.lisp | 2 | ||||
| -rw-r--r-- | consecutive-fibonacci-numbers-are-coprime.lisp | 3 | ||||
| -rw-r--r-- | divisor-list.lisp | 1 | ||||
| -rw-r--r-- | fast-expt.lisp | 2 | ||||
| -rw-r--r-- | flist.lisp | 2 | ||||
| -rw-r--r-- | list-monad.lisp | 1 | ||||
| -rw-r--r-- | palindrome-sandwich.lisp | 1 | ||||
| -rw-r--r-- | peano.lisp | 2 | ||||
| -rw-r--r-- | permutations.lisp | 2 | ||||
| -rw-r--r-- | pigeonhole.lisp | 2 | ||||
| -rw-r--r-- | units.lisp | 2 |
13 files changed, 23 insertions, 1 deletions
@@ -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)) @@ -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) @@ -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) @@ -1,3 +1,5 @@ +(in-package "ACL2") + (defun m (x) x) |