		Search-engine friendly clone of the ACL2 documentation.

Oslib

Basenames

Removing leading directories from a list of paths.

Signature
(basenames paths &key (state 'state)) → (mv err basenames state)
Arguments: paths — Guard (string-listp paths).
Returns: err — NIL on success or an error msg on failure.; basenames — Sensible only if there is no error.
Type (string-listp basenames).; state — Type (state-p1 state), given (force (state-p1 state)).

This just calls basename on every path in a list.

Definitions and Theorems

Function: basenames-fn

(defun basenames-fn (paths state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (string-listp paths)))
  (let ((__function__ 'basenames))
    (declare (ignorable __function__))
    (b* (((when (atom paths)) (mv nil nil state))
         ((mv err name1 state)
          (basename (car paths)))
         ((when err) (mv err nil state))
         ((mv err names2 state)
          (basenames (cdr paths)))
         ((when err) (mv err nil state)))
      (mv nil (cons name1 names2) state))))

Theorem: string-listp-of-basenames.basenames

(defthm string-listp-of-basenames.basenames
  (b* (((mv ?err ?basenames acl2::?state)
        (basenames-fn paths state)))
    (string-listp basenames))
  :rule-classes :rewrite)

Theorem: state-p1-of-basenames.state

(defthm state-p1-of-basenames.state
  (implies (force (state-p1 state))
           (b* (((mv ?err ?basenames acl2::?state)
                 (basenames-fn paths state)))
             (state-p1 state)))
  :rule-classes :rewrite)