		Search-engine friendly clone of the ACL2 documentation.

Std/system

Genvar$

A logic-mode guard-verified version of genvar.

Signature
(genvar$ pkg-witness prefix n avoid-lst state) → var
Arguments: pkg-witness — Guard (symbolp pkg-witness).; prefix — Guard (stringp prefix).; n — Guard (maybe-natp n).; avoid-lst — Guard (symbol-listp avoid-lst).
Returns: var — Type (symbolp var).

This has a stronger guard than genvar and always returns a symbol (if it does not cause an error). We use magic-ev-fncall to call genvar, and check that the result is a symbol. Hard errors happening in genvar are not suppressed, i.e. cause genvar$ to stop with those hard errors. If magic-ev-fncall fails, or if the result is not a symbol, we also stop with hard errors.

Compared to genvar, this utility requires a state argument. It may also be slightly less efficient due the magic-ev-fncall overhead. However, it can be used in logic-mode guard-verified code that follows a statically typed discipline.

Definitions and Theorems

Function: genvar$

(defun
   genvar$
   (pkg-witness prefix n avoid-lst state)
   (declare (xargs :stobjs (state)))
   (declare (xargs :guard (and (symbolp pkg-witness)
                               (stringp prefix)
                               (maybe-natp n)
                               (symbol-listp avoid-lst))))
   (let ((__function__ 'genvar$))
        (declare (ignorable __function__))
        (b* (((mv erp var)
              (magic-ev-fncall 'genvar
                               (list pkg-witness prefix n avoid-lst)
                               state nil t))
             ((when erp)
              (raise "Internal error: ~@0" var))
             ((unless (symbolp var))
              (raise "Internal error: ~x0 is not a symbol."
                     var)))
            var)))

Theorem: symbolp-of-genvar$

(defthm symbolp-of-genvar$
        (b* ((var (genvar$ pkg-witness prefix n avoid-lst state)))
            (symbolp var))
        :rule-classes :rewrite)