• 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
      • Defines
      • Define-sk
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
        • Defiso-implementation
          • Defiso-lookup
          • Defiso-macro-definition
      • 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

• Defiso-implementation

Defiso-macro-definition

Definition of the defiso macro.

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

Macro: defiso

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