		Search-engine friendly clone of the ACL2 documentation.

Glmc-fsm-p

Make-glmc-fsm

Constructor macro for glmc-fsm-p structures.

Syntax:

(make-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 our preferred way to construct glmc-fsm-p structures. It simply conses together a structure with the specified fields.

This macro generates a new glmc-fsm-p structure from scratch. See also change-glmc-fsm, which can "change" an existing structure, instead.

The glmc-fsm-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-glmc-fsm instead.

Definition

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

Macro: make-glmc-fsm

(defmacro make-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-glmc-fsm
                       nil))