read-file-characters-no-error

Included Books

other

(in-package "ACL2")

include-book

(include-book "read-file-characters")

local

(local (include-book "tools/mv-nth" :dir :system))

read-file-characters-no-errorfunction

(defund read-file-characters-no-error
  (filename state)
  (declare (xargs :guard (and (stringp filename) (state-p state))))
  (declare (xargs :stobjs (state)))
  (b* (((mv data state) (read-file-characters filename state)) ((when (stringp data)) (mv (er hard? 'read-file-characters-no-error data) state)))
    (mv data state)))

local

(local (in-theory (enable read-file-characters-no-error)))

state-p1-of-read-file-characters-no-errortheorem

(defthm state-p1-of-read-file-characters-no-error
  (implies (and (force (state-p1 state)) (force (stringp filename)))
    (state-p1 (mv-nth 1 (read-file-characters-no-error filename state)))))

read-file-characters-no-error-returns-character-listtheorem

(defthm read-file-characters-no-error-returns-character-list
  (character-listp (mv-nth 0 (read-file-characters-no-error filename state))))