• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
        • Ps
        • Basic-printing
        • Verilog-printing
        • Printing-locally
        • Formatted-printing
        • Accessing-printed-output
        • Vl-printedlist
        • Json-printing
          • Json-encoders
            • Vl-jp-module
            • Vl-jp-warning
            • Vl-jp-constint
            • Vl-jp-vardecl
            • Jp-sym-main
            • Vl-jp-fundecl
            • Vl-jp-taskdecl
            • Vl-jp-modinst
            • Vl-jp-gateinst
            • Vl-jp-portdecl
            • Vl-jp-modport-port
            • Vl-jp-interfaceport
            • Vl-jp-expr
            • Vl-jp-assign
            • Jp-str
            • Vl-jp-warninglist
            • Vl-jp-vardecllist
            • Vl-jp-taskdecllist
            • Vl-jp-regularportlist
            • Vl-jp-portdecllist
            • Vl-jp-plainarglist
            • Vl-jp-paramvaluelist
            • Vl-jp-paramdecllist
            • Vl-jp-paramdecl
            • Vl-jp-packeddimensionlist
            • Vl-jp-namedparamvaluelist
            • Vl-jp-namedarglist
            • Vl-jp-modport-portlist
            • Vl-jp-modinstlist
            • Vl-jp-modelementlist
            • Vl-jp-interfaceportlist
            • Vl-jp-initiallist
            • Vl-jp-genelementlist
            • Vl-jp-gateinstlist
            • Vl-jp-fwdtypedef
            • Vl-jp-fundecllist
            • Vl-jp-enumitemlist
            • Jp-nat
            • Vl-jp-weirdint
            • Vl-jp-repeateventcontrol
            • Vl-jp-regularport
            • Vl-jp-rangelist
            • Vl-jp-portlist
            • Vl-jp-plainarg
            • Vl-jp-namedparamvalue
            • Vl-jp-namedarg
            • Vl-jp-modulelist
            • Vl-jp-modport
            • Vl-jp-location
            • Vl-jp-initial
            • Vl-jp-importlist
            • Vl-jp-import
            • Vl-jp-genvarlist
            • Vl-jp-genvar
            • Vl-jp-gatestrength
            • Vl-jp-gatedelay
            • Vl-jp-eventcontrol
            • Vl-jp-evatomlist
            • Vl-jp-enumitem
            • Vl-jp-enumbasetype
            • Vl-jp-assignlist
            • Vl-jp-alwayslist
            • Vl-jp-always
            • Vl-jp-aliaslist
            • Vl-jp-alias
            • Jp-object
            • Vl-jp-time
            • Vl-jp-sysfunname
            • Vl-jp-range
            • Vl-jp-evatom
            • Vl-jp-delaycontrol
            • Vl-jp-basictype
            • Vl-jp-typename
            • Vl-jp-tagname
            • Vl-jp-string
            • Vl-jp-real
            • Vl-jp-keyguts
            • Vl-jp-id
            • Vl-jp-hidpiece
            • Vl-jp-funname
            • Vl-jp-extint
            • Vl-jp-arguments
            • Vl-jp-paramvalue
            • Vl-jp-packeddimension
            • Vl-jp-maybe-packeddimension
            • Vl-jp-maybe-nettypename
            • Vl-jp-maybe-direction
            • Vl-jp-maybe-cstrength
            • Jp-timeunit
            • Jp-keygutstype
            • Jp-bool
            • Jp-bitlist
            • Jp-bit
            • Jp-bignat
            • Jp-basictypekind
            • Vl-jp-randomqualifier
            • Vl-jp-port
            • Vl-jp-nettypename
            • Vl-jp-maybe-gatedelay
            • Vl-jp-maybe-exprtype
            • Vl-jp-lifetime
            • Vl-jp-gatetype
            • Vl-jp-exprtype
            • Vl-jp-evatomtype
            • Vl-jp-dstrength
            • Vl-jp-direction
            • Vl-jp-deassign-type
            • Vl-jp-cstrength
            • Vl-jp-coretypename
            • Vl-jp-casetype
            • Vl-jp-casecheck
            • Vl-jp-assign-type
            • Vl-jp-alwaystype
            • Jp-maybe-string
            • Jp-maybe-nat
            • Jp-sym
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Json-encoders

Jp-maybe-nat

Signature

(jp-maybe-nat x &key (ps 'ps)) → ps

Arguments

x — Guard (maybe-natp x).

Definitions and Theorems

Function: jp-maybe-nat-fn

(defun jp-maybe-nat-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (maybe-natp x)))
  (let ((__function__ 'jp-maybe-nat))
    (declare (ignorable __function__))
    (if x (jp-nat x)
      (vl-print-str "null"))))