• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Soft
        • Bv
        • Imp-language
        • C
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
              • Atj-input-processing
              • Atj-java-pretty-printer
                • Jexpr-rank
                • Print-jexprs
                • Print-jchar
                • Print-jstatems+jblocks
                • Print-jclasses+jcmembers
                • Jbinop-expected-ranks
                • Jexpr->rank
                • Jexpr-rank-<=
                • Print-jexpr
                  • Print-jexpr-list
                  • Print-optional-integer-type-suffix
                  • Print-octdig/uscore-list
                  • Print-oct-integer-literal
                  • Print-jcunit
                  • Print-hexdig/uscore-list
                  • Print-hex-integer-literal
                  • Print-decdig/uscore-list
                  • Print-dec-integer-literal
                  • Print-bindig/uscore-list
                  • Print-bin-integer-literal
                  • Print-integer-literal
                  • Print-octdig/uscore
                  • Print-jmethod
                  • Print-jfield
                  • Print-hexdig/uscore
                  • Print-decdig/uscore
                  • Print-bindig/uscore
                  • Print-jclass-list
                  • Print-jlocvar
                  • Print-jliteral
                  • Print-jcinitializer
                  • Print-jline
                  • Print-jimports
                  • Print-jchars
                  • Print-comma-sep
                  • Print-jimport
                  • Print-jbinop
                  • Print-primitive-type
                  • Print-jparam-list
                  • Print-jlines-to-channel
                  • Jexpr-rank-index
                  • Atj-indent
                  • Print-to-jfile
                  • Print-jparam
                  • Print-jaccess
                  • Print-oct-digit
                  • Print-junop
                  • Print-jtype
                  • Print-jresult
                  • Print-hex-digit
                  • Print-dec-digit
                  • Print-bin-digit
                  • Print-jline-blank
                • Atj-code-generation
                • Atj-java-primitives
                • Atj-java-primitive-arrays
                • Atj-type-macros
                • Atj-java-syntax-operations
                • Atj-fn
                • Atj-library-extensions
                • Atj-java-input-types
                • Atj-test-structures
                • Aij-notions
                • Atj-macro-definition
              • Atj-tutorial
            • Aij
            • Language
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Number-theory
          • Cryptography
          • Lists-light
          • Builtins
          • Axe
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Print-jexpr

    Print-jexpr-list

    Signature
    (print-jexpr-list exprs expected-rank) → parts
    Arguments
    exprs — Guard (jexpr-listp exprs).
    expected-rank — Guard (jexpr-rankp expected-rank).
    Returns
    parts — Type (msg-listp parts).