• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
            • Abstract-syntax
              • Tyspecseq
              • Expr
              • Binop
              • Fileset
              • Obj-declor
              • Ident
              • Iconst
              • Obj-adeclor
              • Abstract-syntax-operations
                • Stmts/blocks-nocallsp
                  • Block-item-nocallsp
                    • Block-item-list-nocallsp
                    • Stmt-nocallsp
                  • Tyspec+declor-to-ident+params+tyname
                  • Fundef-list-to-fun-declon-list
                  • Fundef-list->name-list
                  • Ident+tyname-to-tyspec+declor
                  • Tyspec+declor-to-ident+tyname
                  • Obj-declon-to-ident+scspec+tyname+init
                  • Ident+adeclor-to-obj-declor
                  • Ident+adeclor-to-fun-declor
                  • Fun-adeclor-to-params+declor
                  • Param-declon-list-to-ident+tyname-lists
                  • Obj-declor-to-ident+adeclor
                  • Fun-declor-to-ident+adeclor
                  • Expr-constp
                  • Fundef-to-fun-declon
                  • Param-declon-to-ident+tyname
                  • Ext-declon-list->fundef-list
                  • Struct-declon-to-ident+tyname
                  • Unop-nonpointerp
                  • Expr-nocallsp
                  • Expr-list-nocallsp
                  • Binop-strictp
                  • Initer-option-nocallsp
                  • Expr-list-constp
                  • Obj-declon-nocallsp
                  • Expr-option-nocallsp
                  • Binop-purep
                  • Initer-nocallsp
                  • Label-nocallsp
                  • Fundef->name
                  • Block-item-nocallsp
                    • Block-item-list-nocallsp
                    • Stmt-nocallsp
                  • Const
                  • Fundef
                  • Unop
                  • File
                  • Tag-declon
                  • Fun-declor
                  • Obj-declon
                  • Iconst-length
                  • Label
                  • Struct-declon
                  • Initer
                  • Ext-declon
                  • Fun-adeclor
                  • Expr-option
                  • Iconst-base
                  • Initer-option
                  • Iconst-option
                  • Tyspecseq-option
                  • Stmt-option
                  • Scspecseq
                  • Param-declon
                  • Obj-declon-option
                  • File-option
                  • Tyname
                  • Transunit
                  • Fun-declon
                  • Transunit-result
                  • Param-declon-list
                  • Struct-declon-list
                  • Expr-list
                  • Tyspecseq-list
                  • Ident-set
                  • Ident-list
                  • Ext-declon-list
                  • Unop-list
                  • Tyname-list
                  • Fundef-list
                  • Fun-declon-list
                  • Binop-list
                  • Stmt-fixtypes
                  • Expr-fixtypes
                • Integer-ranges
                • Implementation-environments
                • Dynamic-semantics
                • Static-semantics
                • Grammar
                • Integer-formats
                • Types
                • Portable-ascii-identifiers
                • Values
                • Integer-operations
                • Computation-states
                • Object-designators
                • Operations
                • Errors
                • Tag-environments
                • Function-environments
                • Character-sets
                • Flexible-array-member-removal
                • Arithmetic-operations
                • Pointer-operations
                • Bytes
                • Keywords
                • Real-operations
                • Array-operations
                • Scalar-operations
                • Structure-operations
              • Representation
              • Transformation-tools
              • Insertion-sort
              • Pack
            • Bv
            • Imp-language
            • Event-macros
            • Java
            • Bitcoin
            • Ethereum
            • Yul
            • Zcash
            • ACL2-programming-language
            • Prime-fields
            • Json
            • Syntheto
            • File-io-light
            • Cryptography
            • Number-theory
            • Lists-light
            • Axe
            • Builtins
            • Solidity
            • Helpers
            • Htclient
            • Typed-lists-light
            • Arithmetic-light
          • X86isa
          • Axe
          • Execloader
        • Math
        • Testing-utilities
      • Abstract-syntax-operations
      • Stmts/blocks-nocallsp

      Block-item-nocallsp

      Check if a block item does not contain any function calls.

      Signature
      (block-item-nocallsp item) → yes/no
      Arguments
      item — Guard (block-itemp item).
      Returns
      yes/no — Type (booleanp yes/no).