Encode a probably small natural number as a JSON number.
(jp-nat x &key (ps 'ps)) → ps
- 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
(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."