		Search-engine friendly clone of the ACL2 documentation.

Vls-commands

Vls-success

Create a "standard", JSON-encoded successful return value for a VL server command.

Signature
(vls-success &key json) → extended-value
Arguments: json — Should be a json-encoded string for the actual value you want to return. This is a keyword argument to remind the caller that they need to provide a json-encoded value.
Guard (stringp json).
Returns: extended-value — Type (stringp extended-value).

Definitions and Theorems

Function: vls-success-fn

(defun vls-success-fn (json)
  (declare (xargs :guard (stringp json)))
  (let ((__function__ 'vls-success))
    (declare (ignorable __function__))
    (cat "{\":ERROR\": false, \":VALUE\": "
         json "}")))

Theorem: stringp-of-vls-success

(defthm stringp-of-vls-success
  (b* ((extended-value (vls-success-fn json)))
    (stringp extended-value))
  :rule-classes :type-prescription)