• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
        • Ps
        • Verilog-printing
        • Basic-printing
        • Printing-locally
        • Formatted-printing
        • Accessing-printed-output
        • Json-printing
          • Json-encoders
            • Vl-jp-expr
            • Vl-jp-module
            • Vl-jp-interface
            • Vl-jp-design
            • Vl-jp-warning
            • Vl-jp-package
            • Vl-jp-vardecl
            • Vl-jp-class
            • Vl-jp-ansi-portdecl
            • Vl-jp-constint
            • Jp-sym-main
            • Vl-jp-udp
            • Vl-jp-taskdecl
            • Vl-jp-fundecl
            • Vl-jp-clkdecl
            • Vl-jp-modinst
            • Vl-jp-gateinst
            • Vl-jp-dpiimport
            • Vl-jp-typedef
            • Vl-jp-propport
            • Vl-jp-program
            • Vl-jp-portdecl
            • Vl-jp-paramdecl
            • Vl-jp-modport-port
            • Vl-jp-interfaceport
            • Vl-jp-dpiexport
            • Vl-jp-config
            • Vl-jp-assign
            • Jp-str
            • Vl-jp-warninglist
            • Vl-jp-vardecllist
            • Vl-jp-udpentrylist
            • Vl-jp-typedeflist
            • Vl-jp-taskdecllist
            • Vl-jp-sequencelist
            • Vl-jp-sequence
            • Vl-jp-propportlist
            • Vl-jp-propertylist
            • Vl-jp-property
            • Vl-jp-programlist
            • Vl-jp-portdecllist
            • Vl-jp-plainarglist
            • Vl-jp-parse-temps
            • Vl-jp-paramvaluelist
            • Vl-jp-paramdecllist
            • Vl-jp-packagelist
            • Vl-jp-namedparamvaluelist
            • Vl-jp-namedarglist
            • Vl-jp-modportlist
            • Vl-jp-modport-portlist
            • Vl-jp-modinstlist
            • Vl-jp-locationlist
            • Vl-jp-interfacelist
            • Vl-jp-initiallist
            • Vl-jp-gclkdecllist
            • Vl-jp-gateinstlist
            • Vl-jp-fwdtypedeflist
            • Vl-jp-fwdtypedef
            • Vl-jp-fundecllist
            • Vl-jp-exprdistlist
            • Vl-jp-elabtasklist
            • Vl-jp-dpiimportlist
            • Vl-jp-dpiexportlist
            • Vl-jp-defaultdisablelist
            • Vl-jp-covergrouplist
            • Vl-jp-clkdecllist
            • Vl-jp-clkassignlist
            • Vl-jp-clkassign
            • Vl-jp-cassertionlist
            • Vl-jp-blockitemlist
            • Vl-jp-bind
            • Vl-jp-assertionlist
            • Vl-jp-ansi-portdecllist
            • Jp-nat
            • Vl-jp-udplist
            • Vl-jp-udplinelist
            • Vl-jp-udpline
            • Vl-jp-timeunitdecl
            • Vl-jp-timeprecisiondecl
            • Vl-jp-repetition
            • Vl-jp-repeateventcontrol
            • Vl-jp-regularport
            • Vl-jp-propspec
            • Vl-jp-portlist
            • Vl-jp-plainarg
            • Vl-jp-namedparamvalue
            • Vl-jp-namedarg
            • Vl-jp-modulelist
            • Vl-jp-modport
            • Vl-jp-initial
            • Vl-jp-importlist
            • Vl-jp-import
            • Vl-jp-genvarlist
            • Vl-jp-gclkdecl
            • Vl-jp-gatestrength
            • Vl-jp-gatedelay
            • Vl-jp-finallist
            • Vl-jp-eventcontrol
            • Vl-jp-distitemlist
            • Vl-jp-distitem
            • Vl-jp-defaultdisable
            • Vl-jp-covergroup
            • Vl-jp-configlist
            • Vl-jp-classlist
            • Vl-jp-bindlist
            • Vl-jp-assignlist
            • Vl-jp-alwayslist
            • Vl-jp-always
            • Vl-jp-aliaslist
            • Vl-jp-alias
            • Jp-object
            • Vl-jp-udpedge
            • Vl-jp-timeliteral
            • Vl-jp-maybe-timeunitdecl
            • Vl-jp-maybe-timeprecisiondecl
            • Vl-jp-maybe-gatestrength
            • Vl-jp-maybe-delayoreventcontrol
            • Vl-jp-genvar
            • Vl-jp-final
            • Vl-jp-exprdist
            • Vl-jp-delaycontrol
            • Vl-jp-clkskew
            • Vl-jp-maybe-udpsymbol
            • Vl-jp-maybe-timeliteral
            • Vl-jp-maybe-scopeid
            • Vl-jp-maybe-rhs
            • Vl-jp-maybe-parse-temps
            • Vl-jp-maybe-paramvalue
            • Vl-jp-maybe-nettypename
            • Vl-jp-maybe-module
            • Vl-jp-maybe-gatedelay
            • Vl-jp-maybe-exprdist
            • Vl-jp-maybe-clkskew
            • Vl-jp-elabtask
            • Vl-jp-weirdint
            • Vl-jp-value
            • Vl-jp-time
            • Vl-jp-string
            • Vl-jp-maybe-direction
            • Vl-jp-maybe-cstrength
            • Vl-jp-extint
            • Jp-timeunit
            • Jp-bool
            • Jp-bitlist
            • Jp-bit
            • Jp-bignat
            • Vl-jp-real
            • Vl-jp-maybe-exprsign
            • Vl-jp-gatetype
            • Vl-jp-exprsign
            • Vl-jp-evatomtype
            • Vl-jp-dstrength
            • Vl-jp-direction
            • Vl-jp-deassign-type
            • Vl-jp-cstrength
            • Vl-jp-casetype
            • Vl-jp-casekey
            • Vl-jp-casecheck
            • Vl-jp-assign-type
            • Vl-jp-alwaystype
            • Jp-maybe-string
            • Jp-maybe-nat
            • Jp-sym
        • Vl-printedlist
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Json-encoders

Jp-bignat

Encode a potentially large natural number as a JSON string.

Signature

(jp-bignat x &key (ps 'ps)) → ps

Arguments

x — Guard (natp x).

Definitions and Theorems

Function: jp-bignat-fn

(defun jp-bignat-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (natp x)))
  (let ((__function__ 'jp-bignat))
    (declare (ignorable __function__))
    (vl-print-str (natstr x))))