• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • 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
                • Exprp
                • Expr-case
                • Expr-binary
                • Expr-equiv
                • Expr-cond
                • Expr-unary
                • Expr-memberp
                • Expr-member
                • Expr-cast
                • Expr-call
                • Expr-arrsub
                • Expr-kind
                • Expr-preinc
                • Expr-predec
                • Expr-postinc
                • Expr-postdec
                • Expr-ident
                • Expr-const
                • Expr-fix
                • Expr-count
                • Binop
                • Fileset
                • Obj-declor
                • Ident
                • Iconst
                • Obj-adeclor
                • Abstract-syntax-operations
                • 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
                  • Expr
                    • Exprp
                    • Expr-case
                    • Expr-binary
                    • Expr-equiv
                    • Expr-cond
                    • Expr-unary
                    • Expr-memberp
                    • Expr-member
                    • Expr-cast
                    • Expr-call
                    • Expr-arrsub
                    • Expr-kind
                    • Expr-preinc
                    • Expr-predec
                    • Expr-postinc
                    • Expr-postdec
                    • Expr-ident
                    • Expr-const
                    • Expr-fix
                    • Expr-count
                    • Expr-list
                • 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
              • Transformation-tools
              • Representation
              • Insertion-sort
              • Pack
            • Bv
            • Imp-language
            • Event-macros
            • Java
            • Riscv
            • 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
      • Expr

      Expr-count

      Measure for recurring over expr structures.

      Signature
      (expr-count x) → count
      Arguments
      x — Guard (exprp x).
      Returns
      count — Type (natp count).