• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
        • Proof-support
        • Abstract-syntax
          • Syntax-abstraction
          • Expression
          • Definition
          • Constraint
          • Definition-option
          • Abstract-syntax-operations
            • Expression-var-list
            • Lookup-definition
            • Constrel
              • Constrel-fix
              • Constrel-equiv
              • Make-constrel
              • Change-constrel
                • Constrel->name
                • Constrel->args
                • Constrelp
              • Constraint-constrels
              • Constraint-list-constrels
              • Constraint-rels
              • Constraint-list-rels
              • Expression-sub
              • Expression-const/var-listp
              • Expression-var-listp
              • Expression-neg
              • Expression-list-vars
              • Expression-vars
              • Definition-free-vars
              • Constraint-vars
              • Constraint-list-vars
              • Constrel-set
            • System
            • Convenience-constructors
            • System-result
            • Expression-result
            • Expression-list-result
            • Definition-result
            • Definition-list-result
            • Constraint-result
            • Constraint-list-result
            • Expression-list
            • Definition-list
            • Constraint-list
          • R1cs-subset
          • Semantics
          • Abstract-syntax-operations
            • Expression-var-list
            • Lookup-definition
            • Constrel
              • Constrel-fix
              • Constrel-equiv
              • Make-constrel
              • Change-constrel
                • Constrel->name
                • Constrel->args
                • Constrelp
              • Constraint-constrels
              • Constraint-list-constrels
              • Constraint-rels
              • Constraint-list-rels
              • Expression-sub
              • Expression-const/var-listp
              • Expression-var-listp
              • Expression-neg
              • Expression-list-vars
              • Expression-vars
              • Definition-free-vars
              • Constraint-vars
              • Constraint-list-vars
              • Constrel-set
            • Indexed-names
            • Well-formedness
            • Concrete-syntax
            • R1cs-bridge
            • Parser-interface
          • Legacy-defrstobj
          • Proof-checker-array
          • Soft
          • C
          • 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
      • Constrel

      Change-constrel

      Modifying constructor for constrel structures.

      Syntax
      (change-constrel x 
                       [:name <name>] 
                       [:args <args>]) 
      

      This is an often useful alternative to make-constrel.

      We construct a new constrel 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-constrel

      (defmacro change-constrel (x &rest args)
        (std::change-aggregate 'constrel
                               x args
                               '((:name . constrel->name)
                                 (:args . constrel->args))
                               'change-constrel
                               'nil))