Написание функции select() в ACL2

Question

Я пытаюсь написать функцию в ACL2 (в частности, ACL2s), которая принимает список и натуральное число и возвращает элемент в списке по указанному индексу. Так (выберите (список 1 2 3) 2) вернет 3.

Вот мой код:

;; 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))

Любая помощь высоко ценится!

Answer 1

Мне кажется, что сообщение довольно ясно: вы пытаетесь получить первый элемент пустого списка, который противоречит вашей спецификации.

Исходя из этой ссылки, кажется, что first ожидает непустой список, тогда как car возвращается nil когда ваш вклад nil,

Либо вы справитесь nil случай явно с endp тест или вы используете car вместо first,