• 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
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
              • Print-exprs/decls/stmts
              • Print-expr
              • Pristate
              • Print-dec/oct/hex-const
              • Priopt
              • Print-fundef
              • Print-filepath-transunit-map
              • Print-s-char
              • Print-c-char
              • Print-q-char
              • Print-h-char
              • Print-fileset
              • Print-typequal/attribspec-list-list
              • Print-file
              • Print-hex-core-fconst
              • Print-dec-core-fconst
              • Print-ident-list
              • Print-fsuffix
              • Print-oct-digit-achar
              • Print-label-declaration-list
              • Print-hex-frac-const
              • Print-hex-digit-achar
              • Print-dec-frac-const
              • Print-dec-digit-achar
              • Print-asm-clobber-list
              • Print-stringlit-list
              • Print-inc/dec-op-list
              • Print-astring
              • Print-asm-name-spec
              • Print-univ-char-name
              • Print-struni-spec
              • Print-simple-escape
              • Print-label-declaration
              • Print-isuffix-option
              • Print-fsuffix-option
              • Print-extdecl-list
              • Print-eprefix-option
              • Print-dec-expo-option
              • Print-cprefix-option
              • Print-binop
              • Print-attrib-name
              • Print-type-qual
              • Print-s-char-list
              • Print-q-char-list
              • Print-indent
              • Print-ident
              • Print-h-char-list
              • Print-dec-expo-prefix
              • Print-char
              • Print-c-char-list
              • Print-bin-expo-prefix
              • Print-asm-qual-list
              • Print-stringlit
              • Print-stor-spec
              • Print-sign-option
              • Print-oct-escape
              • Print-header-name
              • Print-extdecl
              • Print-escape
              • Print-cconst
              • Print-asm-qual
              • Print-asm-clobber
              • Init-pristate
              • Dec-pristate-indent
              • Print-isuffix
              • Print-fun-spec
              • Print-fconst
              • Print-dec-expo
              • Print-bin-expo
              • Print-unop
              • Print-transunit
              • Print-new-line
              • Print-lsuffix
              • Print-inc/dec-op
              • Print-hex-quad
              • Print-eprefix
              • Print-cprefix
              • Print-usuffix
              • Print-iconst
              • Print-hprefix
              • Print-const
              • Print-comp-stmt
              • Print-hex-digit-achars
              • Print-sign
              • Print-oct-digit-achars
              • Print-dec-digit-achars
              • Print-chars
              • Inc-pristate-indent
              • Print-expr-list
              • Print-struct-declon-list
              • Print-stmt
              • Print-param-declor
              • Print-dirdeclor
              • Default-priopt
              • Print-struct-declor
              • Print-initer
              • Print-decl-inline
              • Print-struct-declon
              • Print-genassoc-list
              • Print-enum-spec
                • Print-absdeclor
                • Print-typequal/attribspec-list
                • Print-desiniter-list
                • Print-const-expr
                • Print-attrib
                • Print-tyname
                • Print-struct-declor-list
                • Print-spec/qual-list
                • Print-param-declon-list
                • Print-param-declon
                • Print-initdeclor-list
                • Print-designor-list
                • Print-decl-spec-list
                • Print-decl-list
                • Print-attrib-spec-list
                • Print-asm-output-list
                • Print-asm-input-list
                • Print-typequal/attribspec
                • Print-statassert
                • Print-spec/qual
                • Print-member-designor
                • Print-initdeclor
                • Print-enumer-list
                • Print-dirabsdeclor
                • Print-desiniter
                • Print-decl-spec
                • Print-decl
                • Print-block-item-list
                • Print-attrib-spec
                • Print-attrib-list
                • Print-asm-output
                • Print-align-spec
                • Print-type-spec
                • Print-label
                • Print-genassoc
                • Print-enumer
                • Print-designor
                • Print-declor
                • Print-block-item
                • Print-asm-stmt
                • Print-asm-input
              • Output-files
              • Abstract-syntax-operations
              • Implementation-environments
              • Abstract-syntax
              • Concrete-syntax
              • Disambiguation
              • Validation
              • Gcc-builtins
              • Preprocessing
              • Parsing
            • Atc
            • Transformation-tools
            • Language
            • Representation
            • Insertion-sort
            • Pack
          • Soft
          • Bv
          • Imp-language
          • Ethereum
          • Event-macros
          • Java
          • Riscv
          • Bitcoin
          • Zcash
          • Yul
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Axe
          • Lists-light
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Printer
    • Print-exprs/decls/stmts

    Print-enum-spec

    Print an enueration specifier.

    Signature
    (print-enum-spec enumspec pstate) → new-pstate
    Arguments
    enumspec — Guard (enum-specp enumspec).
    pstate — Guard (pristatep pstate).
    Returns
    new-pstate — Type (pristatep new-pstate).

    We ensure that the enumeration specifier is not empty, i.e. that there is a name or a non-empty list of enumerators.