• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
        • Defsurj
        • Defiso
        • Defmapping-implementation
          • Defmapping-event-generation
          • Defmapping-check-redundancy
          • Defmapping-table
            • Defmapping-infop
              • Defmapping-info
              • Make-defmapping-info
              • Change-defmapping-info
              • Honsed-defmapping-info
              • Make-honsed-defmapping-info
              • Defmapping-info->unconditional
              • Defmapping-info->expansion
              • Defmapping-info->domb-guard
              • Defmapping-info->domb
              • Defmapping-info->doma-guard
              • Defmapping-info->doma
              • Defmapping-info->call$
              • Defmapping-info->beta-of-alpha
              • Defmapping-info->beta-injective
              • Defmapping-info->beta-image
              • Defmapping-info->beta-guard
              • Defmapping-info->beta
              • Defmapping-info->alpha-of-beta
              • Defmapping-info->alpha-injective
              • Defmapping-info->alpha-image
              • Defmapping-info->alpha-guard
              • Defmapping-info->alpha
            • Defmapping-lookup
            • Defmapping-filter-call
            • Maybe-defmapping-infop
            • *defmapping-table-name*
          • Defmapping-fn
          • Defmapping-input-processing
          • Defmapping-macro-definition
        • Definj
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Define-sk
      • Defines
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
      • Defmvtypes
      • Defconsts
      • Defthm-unsigned-byte-p
      • Support
      • Defthm-signed-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defmapping-infop

Honsed-defmapping-info

Raw constructor for honsed defmapping-infop structures.

Syntax:

(honsed-defmapping-info call$ expansion doma domb alpha beta
                        alpha-image beta-image beta-of-alpha
                        alpha-of-beta alpha-injective
                        beta-injective doma-guard domb-guard
                        alpha-guard beta-guard unconditional)

This is identical to defmapping-info, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by std::defaggregate.

Function: honsed-defmapping-info

(defun honsed-defmapping-info
       (call$ expansion doma domb alpha beta
              alpha-image beta-image beta-of-alpha
              alpha-of-beta alpha-injective
              beta-injective doma-guard domb-guard
              alpha-guard beta-guard unconditional)
 (declare (xargs :guard (and (pseudo-event-formp call$)
                             (pseudo-event-formp expansion)
                             (pseudo-termfnp doma)
                             (pseudo-termfnp domb)
                             (pseudo-termfnp alpha)
                             (pseudo-termfnp beta)
                             (symbolp alpha-image)
                             (symbolp beta-image)
                             (symbolp beta-of-alpha)
                             (symbolp alpha-of-beta)
                             (symbolp alpha-injective)
                             (symbolp beta-injective)
                             (symbolp doma-guard)
                             (symbolp domb-guard)
                             (symbolp alpha-guard)
                             (symbolp beta-guard)
                             (booleanp unconditional))))
 (mbe
  :logic (defmapping-info call$ expansion doma domb alpha beta
                          alpha-image beta-image beta-of-alpha
                          alpha-of-beta alpha-injective
                          beta-injective doma-guard domb-guard
                          alpha-guard beta-guard unconditional)
  :exec
  (hons
   (hons 'call$ call$)
   (hons
    (hons 'expansion expansion)
    (hons
     (hons 'doma doma)
     (hons
      (hons 'domb domb)
      (hons
       (hons 'alpha alpha)
       (hons
        (hons 'beta beta)
        (hons
         (hons 'alpha-image alpha-image)
         (hons
          (hons 'beta-image beta-image)
          (hons
           (hons 'beta-of-alpha beta-of-alpha)
           (hons
            (hons 'alpha-of-beta alpha-of-beta)
            (hons
             (hons 'alpha-injective alpha-injective)
             (hons
              (hons 'beta-injective beta-injective)
              (hons
               (hons 'doma-guard doma-guard)
               (hons
                (hons 'domb-guard domb-guard)
                (hons
                     (hons 'alpha-guard alpha-guard)
                     (hons (hons 'beta-guard beta-guard)
                           (hons (hons 'unconditional unconditional)
                                 nil)))))))))))))))))))