		Search-engine friendly clone of the ACL2 documentation.

Omaps

Head-val

Value associated to the smallest key of a non-empty omap.

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

This is used as an abbreviation, so it is enabled by default.

Definitions and Theorems

Function: head-val

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