		Search-engine friendly clone of the ACL2 documentation.

States32i

Stat32i-from-stat

Convert from stat-rv32i-p to stat32i.

Signature
(stat32i-from-stat stat) → stat32i
Arguments: stat — Guard (stat-rv32i-p stat).
Returns: stat32i — Type (stat32ip stat32i).

Definitions and Theorems

Function: stat32i-from-stat

(defun stat32i-from-stat (stat)
  (declare (xargs :guard (stat-rv32i-p stat)))
  (let ((__function__ 'stat32i-from-stat))
    (declare (ignorable __function__))
    (make-stat32i :xregs (stat->xregs stat)
                  :pc (stat->pc stat)
                  :memory (stat->memory stat)
                  :error (stat->error stat))))

Theorem: stat32ip-of-stat32i-from-stat

(defthm stat32ip-of-stat32i-from-stat
  (b* ((stat32i (stat32i-from-stat stat)))
    (stat32ip stat32i))
  :rule-classes :rewrite)