• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
        • Deftagsum
        • Defprod
        • Defflexsum
        • Defbitstruct
        • Deflist
        • Defalist
        • Defbyte
        • Defresult
        • Deffixequiv
          • Deffixequiv-sk
            • Deffixequiv-sk-implementation
              • Deffixequiv-sk-lemma-insts-arg
              • Deffixequiv-sk-lemma-insts-args
              • Deffixequiv-sk-hints
              • Deffixequiv-sk-lemma-inst-subst
              • Deffixequiv-sk-fn
              • Deffixequiv-sk-macro-definition
            • Fixequiv-hook
            • Set-fixequiv-guard-override
          • Deffixtype
          • Defoption
          • Fty-discipline
          • Fold
          • Specific-types
          • Fty-extensions
          • Defsubtype
          • Deftypes
          • Defset
          • Defflatsum
          • Deflist-of-len
          • Defomap
          • Defbytelist
          • Fty::basetypes
          • Defvisitors
          • Deffixtype-alias
          • Deffixequiv-sk
            • Deffixequiv-sk-implementation
              • Deffixequiv-sk-lemma-insts-arg
              • Deffixequiv-sk-lemma-insts-args
              • Deffixequiv-sk-hints
              • Deffixequiv-sk-lemma-inst-subst
              • Deffixequiv-sk-fn
              • Deffixequiv-sk-macro-definition
            • Defunit
            • Multicase
            • Deffixequiv-mutual
            • Fty::baselists
            • Def-enumcase
            • Defmap
          • Apt
          • Std/util
          • 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
      • Deffixequiv-sk-implementation

      Deffixequiv-sk-macro-definition

      Definition of the deffixequiv-sk macro.

      Macro: deffixequiv-sk

      (defmacro deffixequiv-sk (fn &key args)
        (cons 'make-event
              (cons (cons 'deffixequiv-sk-fn
                          (cons (cons 'quote (cons fn 'nil))
                                (cons (cons 'quote (cons args 'nil))
                                      '((w state)))))
                    'nil)))