		Search-engine friendly clone of the ACL2 documentation.

Glmc-fsm-p

Make-honsed-glmc-fsm

Constructor macro for honsed glmc-fsm-p structures.

Syntax:

(make-honsed-glmc-fsm [:nextst <nextst>] 
                      [:prop <prop>] 
                      [:fsm-constr <fsm-constr>] 
                      [:bit-constr <bit-constr>] 
                      [:initst <initst>] 
                      [:st-hyp <st-hyp>] 
                      [:hyp <hyp>] 
                      [:st-hyp-next <st-hyp-next>] 
                      [:interp-clauses <interp-clauses>] 
                      [:hyp-var-bound <hyp-var-bound>] 
                      [:var-bound <var-bound>])

This is identical to make-glmc-fsm, except that we hons the structure we are creating.

Definition

This is an ordinary honsing make- macro introduced by std::defaggregate.

Macro: make-honsed-glmc-fsm

(defmacro make-honsed-glmc-fsm (&rest args)
  (std::make-aggregate 'glmc-fsm
                       args
                       '((:nextst)
                         (:prop)
                         (:fsm-constr)
                         (:bit-constr)
                         (:initst)
                         (:st-hyp)
                         (:hyp)
                         (:st-hyp-next)
                         (:interp-clauses)
                         (:hyp-var-bound)
                         (:var-bound))
                       'make-honsed-glmc-fsm
                       t))