		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-rel-name

Lift a PFCS relation name to an ACL2 symbol.

Signature
(lift-rel-name name wrld) → sym
Arguments: name — Guard (stringp name).; wrld — Guard (plist-worldp wrld).
Returns: sym — Type (symbolp sym).

The symbol is the lifted predicate name, which we retrieve from the table of lifted PFCSes. If it is not in the table, which happens when we are lifting the PFCS definition of the relation, for now we use the same mapping as for the variables.

Definitions and Theorems

Function: lift-rel-name

(defun lift-rel-name (name wrld)
  (declare (xargs :guard (and (stringp name)
                              (plist-worldp wrld))))
  (let ((__function__ 'lift-rel-name))
    (declare (ignorable __function__))
    (b* ((tab (table-alist+ 'lift-table wrld))
         (info (cdr (assoc-equal name tab)))
         ((unless info)
          (raise "Internal error: ~x0 not in table."
                 name))
         ((unless (lift-infop info))
          (raise "Internal error: ~x0 has the wrong type."
                 info)))
      (lift-info->pred info))))

Theorem: symbolp-of-lift-rel-name

(defthm symbolp-of-lift-rel-name
  (b* ((sym (lift-rel-name name wrld)))
    (symbolp sym))
  :rule-classes :rewrite)