		Search-engine friendly clone of the ACL2 documentation.

Omaps

Head-key

Smallest key of a non-empty omap.

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

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

Definitions and Theorems

Function: head-key

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