• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Soft
        • Bv
        • Imp-language
        • C
          • Syntax-for-tools
            • Disambiguator
            • Abstract-syntax
            • Parser
            • Validator
            • Printer
              • Print-exprs/decls/stmts
              • Print-expr
              • Pristate
              • Print-fileset
              • Print-dec/oct/hex-const
              • Priopt
              • Print-fundef
              • Print-s-char
              • Print-c-char
              • Print-typequal/attribspec-list-list
              • Print-ident
              • Print-ident-list
              • Print-hex-core-fconst
              • Print-dec-core-fconst
              • Print-oct-digit-achar
              • Print-hex-frac-const
              • Print-hex-digit-achar
              • Print-dec-frac-const
              • Print-dec-digit-achar
              • Print-strunispec
              • Print-file
              • Print-astring
              • Print-asm-name-spec
              • Print-asm-clobber-list
              • Print-stringlit-list
              • Print-inc/dec-op-list
              • Print-cprefix-option
              • Print-binop
              • Print-univ-char-name
              • Print-type-qual
              • Print-transunit
              • Print-simple-escape
              • Print-s-char-list
              • Print-isuffix-option
              • Print-indent
              • Print-fsuffix-option
              • Print-extdecl-list
              • Print-eprefix-option
              • Print-dec-expo-option
              • Print-char
              • Print-c-char-list
              • Print-attrib-name
              • Print-asm-qual-list
              • Print-stor-spec
              • Print-oct-escape
              • Print-escape
              • Print-dec-expo-prefix
              • Print-cconst
              • Print-bin-expo-prefix
              • Dec-pristate-indent
              • Print-stringlit
              • Print-sign-option
              • Print-isuffix
              • Print-fun-spec
              • Print-fconst
              • Print-extdecl
              • Print-dec-expo
              • Print-block
              • Print-bin-expo
              • Print-asm-qual
              • Print-asm-clobber
              • Print-new-line
              • Print-lsuffix
              • Print-inc/dec-op
              • Print-hex-quad
              • Print-fsuffix
              • Print-eprefix
              • Print-cprefix
              • Print-usuffix
              • Print-unop
              • Print-iconst
              • Print-hprefix
              • Print-const
              • Print-chars
              • Print-sign
              • Print-oct-digit-achars
              • Print-hex-digit-achars
              • Print-dec-digit-achars
              • Print-stmt
              • Print-expr-list
              • Init-pristate
              • Print-structdecl-list
              • Inc-pristate-indent
              • Print-paramdeclor
              • Print-dirdeclor
              • Default-priopt
              • Print-structdeclor
              • Print-initer
              • Print-decl-inline
              • Print-structdecl
              • Print-genassoc-list
              • Print-enumspec
              • Print-absdeclor
              • Print-typequal/attribspec-list
              • Print-desiniter-list
              • Print-const-expr
              • Print-attrib
              • Print-tyname
              • Print-structdeclor-list
              • Print-spec/qual-list
              • Print-paramdecl-list
              • Print-paramdecl
              • 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
              • Formalized-subset
              • Mapping-to-language-definition
              • Defpred
              • Output-files
              • Input-files
              • Abstract-syntax-operations
              • Implementation-environments
              • Concrete-syntax
              • Unambiguity
              • Preprocessing
              • Abstraction-mapping
              • Annotation
            • Atc
            • Language
            • Representation
            • Transformation-tools
            • Pack
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Number-theory
          • Cryptography
          • Lists-light
          • Builtins
          • Axe
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Printer
    • Print-exprs/decls/stmts

    Print-label

    Print a label.

    Signature
    (print-label label pstate) → new-pstate
    Arguments
    label — Guard (labelp label).
    pstate — Guard (pristatep pstate).
    Returns
    new-pstate — Type (pristatep new-pstate).