• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
        • Open-channel-lemmas
        • Std/io/read-char$
        • Std/io/read-object
        • Std/io/open-output-channel
        • Unsound-read
        • Read-string
        • Read-bytes$
        • File-measure
        • Read-bytes$-n
        • Std/io/read-byte$
        • Std/io/open-input-channel
        • Read-file-lines-no-newlines
        • Print-compressed
        • Nthcdr-bytes
        • Read-file-lines
        • Std/io/close-output-channel
        • Read-file-characters
          • Read-char$-all
            • Tr-read-char$-all
          • Read-file-bytes
          • Print-legibly
          • Std/io/close-input-channel
          • Read-file-objects
          • Logical-story-of-io
          • Take-bytes
          • Std/io/peek-char$
          • Read-file-characters-rev
          • Read-file-as-string
          • Std/io/write-byte$
          • Std/io/set-serialize-character
          • Std/io/print-object$
          • Std/io/princ$
          • Std/io/read-file-into-string
          • *file-types*
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Read-char$-all

    Tr-read-char$-all

    Signature
    (tr-read-char$-all channel state acc) → (mv * state)
    Arguments
    channel — Guard (symbolp channel).

    Definitions and Theorems

    Function: tr-read-char$-all

    (defun tr-read-char$-all (channel state acc)
      (declare (xargs :stobjs (state)))
      (declare (xargs :guard (symbolp channel)))
      (declare (xargs :guard (open-input-channel-p channel
                                                   :character state)))
      (let ((__function__ 'tr-read-char$-all))
        (declare (ignorable __function__))
        (b* (((unless (mbt (state-p state)))
              (mv acc state))
             ((mv char state)
              (read-char$ channel state))
             ((unless char) (mv acc state))
             (acc (cons (mbe :logic (char-fix char) :exec char)
                        acc)))
          (tr-read-char$-all channel state acc))))