(vl-extend-def-map name ctx map) → new-map
Function:
(defun vl-extend-def-map (name ctx map) (declare (xargs :guard (and (stringp name) (vl-def-context-p ctx) (vl-def-use-map-p map)))) (let ((__function__ 'vl-extend-def-map)) (declare (ignorable __function__)) (b* ((name (string-fix name)) (ctx (vl-def-context-fix ctx)) (map (vl-def-use-map-fix map)) (prev-uses (cdr (hons-get name map))) (new-uses (cons ctx prev-uses))) (hons-acons name new-uses map))))
Theorem:
(defthm vl-def-use-map-p-of-vl-extend-def-map (b* ((new-map (vl-extend-def-map name ctx map))) (vl-def-use-map-p new-map)) :rule-classes :rewrite)
Theorem:
(defthm vl-extend-def-map-of-str-fix-name (equal (vl-extend-def-map (str-fix name) ctx map) (vl-extend-def-map name ctx map)))
Theorem:
(defthm vl-extend-def-map-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-extend-def-map name ctx map) (vl-extend-def-map name-equiv ctx map))) :rule-classes :congruence)
Theorem:
(defthm vl-extend-def-map-of-vl-def-context-fix-ctx (equal (vl-extend-def-map name (vl-def-context-fix ctx) map) (vl-extend-def-map name ctx map)))
Theorem:
(defthm vl-extend-def-map-vl-def-context-equiv-congruence-on-ctx (implies (vl-def-context-equiv ctx ctx-equiv) (equal (vl-extend-def-map name ctx map) (vl-extend-def-map name ctx-equiv map))) :rule-classes :congruence)
Theorem:
(defthm vl-extend-def-map-of-vl-def-use-map-fix-map (equal (vl-extend-def-map name ctx (vl-def-use-map-fix map)) (vl-extend-def-map name ctx map)))
Theorem:
(defthm vl-extend-def-map-vl-def-use-map-equiv-congruence-on-map (implies (vl-def-use-map-equiv map map-equiv) (equal (vl-extend-def-map name ctx map) (vl-extend-def-map name ctx map-equiv))) :rule-classes :congruence)