		Search-engine friendly clone of the ACL2 documentation.

Json-encoders

Jp-nat

Encode a probably small natural number as a JSON number.

Signature
(jp-nat x &key (ps 'ps)) → ps
Arguments: x — Guard (natp x).

We require that the integer is at most 2^31, which we think is the minimum reasonable size for a JSON implementation to support.

Definitions and Theorems

Function: jp-nat-fn

(defun jp-nat-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (natp x)))
  (let ((__function__ 'jp-nat))
    (declare (ignorable __function__))
    (b* (((unless (<= x (expt 2 31)))
          (raise "Scarily trying to JSON-encode large natural: ~x0."
                 x)
          ps))
      (vl-print-nat x))))