• 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
        • Set
        • Soft
        • 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
                • Priopt-fix
                • Priopt-equiv
                • Make-priopt
                • Priopt->paren-nested-conds
                • Priopt->indent-size
                • Change-priopt
                  • Prioptp
                • 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-param-declor
                • 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-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
              • Formalized-subset
              • Mapping-to-language-definition
              • Input-files
              • Defpred
              • Output-files
              • Abstract-syntax-operations
              • Validation-information
              • Implementation-environments
              • Concrete-syntax
              • Unambiguity
              • Ascii-identifiers
              • Preprocessing
              • Abstraction-mapping
            • Atc
            • Language
            • Representation
            • Transformation-tools
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • 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
    • Priopt

    Change-priopt

    Modifying constructor for priopt structures.

    Syntax
    (change-priopt x 
                   [:indent-size <indent-size>] 
                   [:paren-nested-conds <paren-nested-conds>]) 
    

    This is an often useful alternative to make-priopt.

    We construct a new priopt structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

    Definition

    This is an ordinary change- macro introduced by fty::defprod.

    Macro: change-priopt

    (defmacro change-priopt (x &rest args)
      (std::change-aggregate
           'priopt
           x args
           '((:indent-size . priopt->indent-size)
             (:paren-nested-conds . priopt->paren-nested-conds))
           'change-priopt
           'nil))