		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)