• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
          • Alias-normalization
          • Svex-design-flatten-and-normalize
          • Svex-design-compile
          • Svex-composition
          • Compile.lisp
            • Svex-normalize-assigns
            • Svex-design-flatten
            • Svex-override-lhrange
            • Svex-override-lhs
            • Aliases-indexed->named-aux
            • Svex-compose-assigns/delays
            • Svex-alist-truncate-by-var-decls
            • Svar-map-truncate-by-var-decls
            • Aliases-to-var-decl-map-aux
            • Aliases-indexed->named
            • Svar-indexed->named-memo
            • Lhs-indexed->named
            • Svar-register-indnamememo
            • Svarlist-indexed->named
            • Maybe-svar-fix
            • Lhs-register-indnamememo
            • Maybe-indname-result
            • Aliases-to-var-decl-map
            • Svar-indexed->named
            • Aliases-boundedp-aux
            • Svex-apply-overrides
            • Indnamememo-to-var-decl-map
            • Indname-result
            • Assigns-compose
            • Delay-svarlist->delays
            • Indnamememo
              • Set-indname
              • Resize-indnames
              • Get-indname
              • Indnames-length
              • Svex-override-vars
              • Delay-svar->delays
              • Assigns-to-overrides
              • Svarlist-collect-delays
              • Svex-overridelist-vars
              • Svex-overridelist-keys
              • Assigns-to-overrides-nrev
              • Var-decl-map
              • Cap-length
            • Assign->segment-drivers
            • Segment-driver-map-resolve
            • Assigns->segment-drivers
          • Moddb
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Indnamememo

    Indnames-length

    Get the length of the indnamememo array.

    In the execution this just gets the array length. The logical definition is just a wrapper for len:

    Function: indnames$a-length

    (defun indnames$a-length (indnamememo$a)
      (declare (xargs :guard (indnamememo$ap indnamememo$a)))
      (len indnamememo$a))