• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
      • 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
        • Definj-implementation
          • Definj-lookup
          • Definj-macro-definition
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/osets
    • Std/io
    • 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

• Definj-implementation

Definj-macro-definition

Definition of the definj macro.

We call defmapping-fn, passing t as :alpha-of-beta-thm and nil as :beta-of-alpha-thm. Furthermore, we set the context to reference definj.

Macro: definj

(defmacro definj (&whole call name doma domb
                         alpha beta &key (unconditional 'nil)
                         (guard-thms 't)
                         (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
          't
          (cons
           '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 ''definj
                                (cons (cons 'quote (cons name 'nil))
                                      'nil)))
                    '(state))))))))))))))))))
   (cons ':suppress-errors
         (cons (not print) 'nil)))))