		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-label

Map a label to a label in the language definition.

Signature
(ldm-label label) → (mv erp label1)
Arguments: label — Guard (labelp label).
Returns: label1 — Type (c::labelp label1).

Definitions and Theorems

Function: ldm-label

(defun ldm-label (label)
  (declare (xargs :guard (labelp label)))
  (declare (xargs :guard (label-unambp label)))
  (let ((__function__ 'ldm-label))
    (declare (ignorable __function__))
    (b* (((reterr) (c::label-default)))
      (label-case label :name
                  (b* (((erp ident1) (ldm-ident label.unwrap)))
                    (retok (c::label-name ident1)))
                  :casexpr
                  (b* (((erp expr)
                        (ldm-expr (const-expr->expr label.expr)))
                       ((when label.range?)
                        (reterr (msg "Unsupported case range ~x0."
                                     (label-fix label)))))
                    (retok (c::label-cas expr)))
                  :default (retok (c::label-default))))))

Theorem: labelp-of-ldm-label.label1

(defthm labelp-of-ldm-label.label1
  (b* (((mv acl2::?erp ?label1)
        (ldm-label label)))
    (c::labelp label1))
  :rule-classes :rewrite)

Theorem: ldm-label-of-label-fix-label

(defthm ldm-label-of-label-fix-label
  (equal (ldm-label (label-fix label))
         (ldm-label label)))

Theorem: ldm-label-label-equiv-congruence-on-label

(defthm ldm-label-label-equiv-congruence-on-label
  (implies (label-equiv label label-equiv)
           (equal (ldm-label label)
                  (ldm-label label-equiv)))
  :rule-classes :congruence)