• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
      • Json-encoding
        • Json-encode-main
        • Json-encode-weird-char
        • Json-encode-atom
        • Json-encode
        • Json-encode-chars
        • Json-encode-char
        • Json-encode-str
        • Json-simple-alist-p
        • Json-comma-and-maybe-newline
      • Security
      • Command
      • In-main-thread
      • Message
      • Start
      • Bindings
      • Stop
      • Try-in-main-thread
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Json-encoding

Json-encode

Top level wrapper for json-encode-main.

Signature

(json-encode x) → x-json

Arguments

x — Any ACL2 object.

Returns

x-json — The JSON-encoded version of x.
    Type (stringp x-json).

This wraps up the accumulator used by json-encode-main and deals with getting the characters into the right order.

Definitions and Theorems

Function: json-encode

(defun json-encode (x)
       (declare (xargs :guard t))
       (let ((__function__ 'json-encode))
            (declare (ignorable __function__))
            (let ((acc (json-encode-main x nil)))
                 (str::rchars-to-string acc))))

Theorem: stringp-of-json-encode

(defthm stringp-of-json-encode
        (b* ((x-json (json-encode x)))
            (stringp x-json))
        :rule-classes :type-prescription)