1
我試圖在ACL2(特別是ACL2s)中編寫一個函數,該函數接受列表和自然數並返回給定索引處列表中的項。所以(選擇(表1 2 3)2)將返回3.在ACL2中寫入select()函數
這裏是我的代碼:
;; select: List x Nat -> All
(defunc select (l n)
:input-contract (and (listp l) (natp n))
:output-contract t
(if (equal 0 n)
(first l)
(select (rest l) (- n 1))))
我收到以下錯誤:
Query: Testing body contracts ...
**Summary of Cgen/testing**
We tested 50 examples across 1 subgoals, of which 48 (48 unique) satisfied
the hypotheses, and found 1 counterexamples and 47 witnesses.
We falsified the conjecture. Here are counterexamples:
[found in : "top"]
-- ((L NIL) (N 0))
Test? found a counterexample.
Body contract falsified in:
-- (ACL2::EXTRA-INFO '(:GUARD (:BODY SELECT)) '(FIRST L))
任何幫助是多少不勝感激!
使用'endp'工作!我曾假設'第一'會接受一個非空列表,但我錯了。謝謝! – camden
@camdenb我很高興它的工作,繼續前進:-) – coredump