• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
        • Defsurj
        • Defiso
        • Defmapping-implementation
          • Defmapping-event-generation
          • Defmapping-check-redundancy
          • Defmapping-table
          • Defmapping-fn
          • Defmapping-input-processing
          • Defmapping-macro-definition
        • Definj
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Defines
      • Define-sk
      • 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
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defmapping-implementation

Defmapping-macro-definition

Definition of the defmapping macro.

Submit the event form generated by defmapping-fn.

Macro: defmapping

(defmacro defmapping
          (&whole call name doma domb
                  alpha beta &key (beta-of-alpha-thm 'nil)
                  (alpha-of-beta-thm 'nil)
                  (guard-thms 't)
                  (unconditional 'nil)
                  (thm-names 'nil)
                  (thm-enable 'nil)
                  (hints 'nil)
                  (print ':result)
                  (show-only 'nil))
 (cons
  'make-event-terse
  (cons
   (cons
    'defmapping-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      (cons 'quote (cons doma 'nil))
      (cons
       (cons 'quote (cons domb 'nil))
       (cons
        (cons 'quote (cons alpha 'nil))
        (cons
         (cons 'quote (cons beta 'nil))
         (cons
          (cons 'quote
                (cons beta-of-alpha-thm 'nil))
          (cons
           (cons 'quote
                 (cons alpha-of-beta-thm 'nil))
           (cons
            (cons 'quote (cons guard-thms 'nil))
            (cons
             (cons 'quote (cons unconditional 'nil))
             (cons
              (cons 'quote (cons thm-names 'nil))
              (cons
               (cons 'quote (cons thm-enable 'nil))
               (cons
                (cons 'quote (cons hints 'nil))
                (cons
                 (cons 'quote (cons print 'nil))
                 (cons
                  (cons 'quote (cons show-only 'nil))
                  (cons
                   (cons 'quote (cons call 'nil))
                   (cons
                    (cons 'cons
                          (cons ''defmapping
                                (cons (cons 'quote (cons name 'nil))
                                      'nil)))
                    '(state))))))))))))))))))
   (cons ':suppress-errors
         (cons (not print) 'nil)))))