• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
          • Gatesimp
          • Aignet-hash-mux
          • Aignet-hash-or
          • Aignet-hash-and
          • Aignet-hash-xor
          • Aignet-hash-iff
          • Aignet-build
          • Patbind-aignet-build
          • Representation
          • Aignet-copy-init
          • Aignet-simplify-marked-with-tracking
          • Aignet-cnf
          • Aignet-simplify-with-tracking
          • Aignet-complete-copy
          • Aignet-eval
          • Semantics
          • Aignet-transforms
          • Aignet-simplify-marked
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Aignet-construction

    Patbind-aignet-build

    B* binder to make a nest of logical functions in an aignet.

    See aignet-build for the non-b*-binder version of this macro. This version makes the bindings created by the macro, such as variables assigned using the := operator, available in the remainder of your b* form.