		Search-engine friendly clone of the ACL2 documentation.

States32i

Stat-from-stat32i

Convert from stat32i to stat-rv32i-p.

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

Definitions and Theorems

Function: stat-from-stat32i

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

Theorem: stat-rv32i-p-of-stat-from-stat32i

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