		Search-engine friendly clone of the ACL2 documentation.

Omaps

Head-val

Signature
(head-val map) → *
Arguments: map — Guard (mapp map).

Definitions and Theorems

Function: head-val

(defun head-val (map)
  (declare (xargs :guard (mapp map)))
  (declare (xargs :guard (not (empty map))))
  (let ((__function__ 'head-val))
    (declare (ignorable __function__))
    (mv-let (key val)
            (head map)
      (declare (ignore key))
      val)))