• 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
        • Defsurj-implementation
          • Defsurj-lookup
          • Defsurj-macro-definition
      • 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/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

• Defsurj-implementation

Defsurj-macro-definition

Definition of the defsurj 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 defsurj.

Macro: defsurj

(defmacro defsurj (&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
          'nil
          (cons
           't
           (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 ''defsurj
                                (cons (cons 'quote (cons name 'nil))
                                      'nil)))
                    '(state))))))))))))))))))
   (cons ':suppress-errors
         (cons (not print) 'nil)))))