		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Jexpr-rank-index

Signature
(jexpr-rank-index rank) → index
Arguments: rank — Guard (jexpr-rankp rank).
Returns: index — Type (natp index).

Definitions and Theorems

Function: jexpr-rank-index

(defun jexpr-rank-index (rank)
  (declare (xargs :guard (jexpr-rankp rank)))
  (let ((__function__ 'jexpr-rank-index))
    (declare (ignorable __function__))
    (jexpr-rank-case rank
                     :expression 15
                     :assignment 14
                     :conditional 13
                     :conditional-or 12
                     :conditional-and 11
                     :inclusive-or 10
                     :exclusive-or 9
                     :and 8
                     :equality 7
                     :relational 6
                     :shift 5
                     :additive 4
                     :multiplicative 3
                     :unary 2
                     :postfix 1
                     :primary 0)))

Theorem: natp-of-jexpr-rank-index

(defthm natp-of-jexpr-rank-index
  (b* ((index (jexpr-rank-index rank)))
    (natp index))
  :rule-classes :rewrite)