• 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
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
        • Deffold-reduce
        • Deffold-map
        • Defmake-self
          • Defmake-self-implementation
            • Defmake-self-event-generation
            • Defmake-self-process-inputs-and-gen-everything
            • Defmake-self-fn
            • Defmake-self-input-processing
            • Defmake-self-macro-definition
      • Specific-types
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defomap
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • 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

• Defmake-self-implementation

Defmake-self-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature

(defmake-self-process-inputs-and-gen-everything args wrld) 
  → 
(mv er? event)

Arguments

args — Guard (true-listp args).

wrld — Guard (plist-worldp wrld).

Returns

er? — Type (acl2::maybe-msgp er?).

event — Type (acl2::pseudo-event-formp event).

Definitions and Theorems

Function: defmake-self-process-inputs-and-gen-everything

(defun defmake-self-process-inputs-and-gen-everything (args wrld)
  (declare (xargs :guard (and (true-listp args)
                              (plist-worldp wrld))))
  (let
    ((__function__ 'defmake-self-process-inputs-and-gen-everything))
    (declare (ignorable __function__))
    (b* (((reterr) '(_))
         (fty-table (acl2::table-alist+ 'flextypes-table
                                        wrld))
         (make-self-table (acl2::table-alist+ 'make-self wrld))
         ((erp type
               parents-presentp parents short-presentp
               short long-presentp long print)
          (defmake-self-process-inputs args)))
      (defmake-self-gen-everything
           type parents-presentp parents
           short-presentp short long-presentp
           long print fty-table make-self-table))))

Theorem: maybe-msgp-of-defmake-self-process-inputs-and-gen-everything.er?

(defthm
   maybe-msgp-of-defmake-self-process-inputs-and-gen-everything.er?
  (b* (((mv ?er? acl2::?event)
        (defmake-self-process-inputs-and-gen-everything args wrld)))
    (acl2::maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-defmake-self-process-inputs-and-gen-everything.event

(defthm
 pseudo-event-formp-of-defmake-self-process-inputs-and-gen-everything.event
 (b* (((mv ?er? acl2::?event)
       (defmake-self-process-inputs-and-gen-everything args wrld)))
   (acl2::pseudo-event-formp event))
 :rule-classes :rewrite)