• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
      • Sys-call+
      • Tshell
        • Tshell-call
        • Tshell-call-unsound
        • Tshell-call-fn1
        • Tshell-ensure
        • Tshell-start
        • Tshell-run-background
        • Tshell-call-unsound-fn1
      • Sys-call-status
      • Sys-call*
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
    • Clex
    • Tshell
      • Tshell-call
      • Tshell-call-unsound
      • Tshell-call-fn1
      • Tshell-ensure
      • Tshell-start
      • Tshell-run-background
      • Tshell-call-unsound-fn1
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Tshell
• Tshell-call-unsound
• Tshell-call-fn1

Tshell-call-unsound-fn1

Unsound variant of tshell-call-fn1 which doesn't take state.

Definitions and Theorems

Theorem: return-type-of-tshell-call-unsound-fn1

(defthm return-type-of-tshell-call-unsound-fn1
  (b* (((mv status lines)
        (tshell-call-unsound-fn1 cmd print save)))
    (and (natp status)
         (string-listp lines))))