firstN

Purpose of exercise

Activities

Terminology

Requirements

  1. Define a function firstN that delivers a list comprised of the first n elements of its second argument (which is  a list)
    Example: (firstN 3 (list 1 2 3 4 5 6 7)) is (list 1 2 3)

Properties

  1. Under appropriate conditions on n, k, and xs, the k-th element of (firstN n xs) is the k-th element of xs
  2. (firstN n xs) ia a true-list when xs is a true-list
  3. (firstN n xs) has n or fewer elements
  4. (firstN n xs) has exactly n elements when xs has at least n elements

ACL2 intrinsics useful in this exercise

Notes