Encode a probably small natural number as a JSON number.
(jp-nat x &key (ps 'ps)) → ps
We require that the integer is at most 2^31, which we think is the minimum reasonable size for a JSON implementation to support.
(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))))