• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Representation
        • Transformation-tools
          • Simpadd0
          • Deftrans
          • Splitgso
          • Constant-propagation
            • Value-to-expr
            • Const-prop-eval-impure-binop-expr
            • Env
            • Const-prop-eval-pure-binop-expr
            • Const-prop-filepath-transunit-map
            • Const-prop-eval-unop-expr
            • Const-prop-transunit-ensemble
            • Const-prop-fundef
            • Value-result-to-option
            • Const-prop-extdecl-list
            • Const-prop-extdecl
            • Zero-valuep
            • Iconst-to-value
            • Const-to-value
            • Expr-to-ident
            • Const-prop-transunit
            • Pure-binopp
            • Const-prop-initdeclor-list
            • Const-prop-initdeclor
            • Const-prop-structdeclor-list
            • Const-prop-structdecl-list
            • Const-prop-param-declon-list
            • Const-prop-initer-option
            • Const-prop-initer
            • Const-prop-expr-option
            • Const-prop-dirabsdeclor-option
            • Const-prop-dirabsdeclor
            • Const-prop-const-expr-option
            • Const-prop-absdeclor-option
            • Const-prop-type-spec
            • Const-prop-strunispec
            • Const-prop-structdeclor
            • Const-prop-structdecl
            • Const-prop-statassert
            • Const-prop-spec/qual-list
            • Const-prop-spec/qual
            • Const-prop-param-declor
            • Const-prop-param-declon
            • Const-prop-member-designor
            • Const-prop-genassoc-list
            • Const-prop-genassoc
            • Const-prop-expr-list
            • Const-prop-expr
            • Const-prop-enumspec
              • Const-prop-enumer-list
              • Const-prop-dirdeclor
              • Const-prop-desiniter-list
              • Const-prop-desiniter
              • Const-prop-designor-list
              • Const-prop-designor
              • Const-prop-declor-option
              • Const-prop-decl-spec-list
              • Const-prop-decl-spec
              • Const-prop-decl-list
              • Const-prop-block-item-list
              • Const-prop-align-spec
              • Const-prop-absdeclor
              • Const-prop-tyname
              • Const-prop-stmt
              • Const-prop-label
              • Const-prop-enumer
              • Const-prop-declor
              • Const-prop-decl
              • Const-prop-const-expr
              • Const-prop-block-item
            • Split-fn
            • Copy-fn
            • Specialize
            • Split-all-gso
            • Rename
            • Utilities
          • Insertion-sort
          • Pack
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Constant-propagation

    Const-prop-enumspec

    Propagate a constant through a enumspec.

    Signature
    (const-prop-enumspec enumspec env) → (mv new-enumspec new-env)
    Arguments
    enumspec — Guard (enumspecp enumspec).
    env — Guard (envp env).
    Returns
    new-enumspec — Type (enumspecp new-enumspec).
    new-env — Type (envp new-env).