		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-console-error

Converts a json-member console error statement to a leo::statement of kind :console

Signature
(j2f-console-error json-console-error) → (mv erp leo-console-error-statement)
Arguments: json-console-error — Guard (json::memberp json-console-error).
Returns: erp — Type (booleanp erp).; leo-console-error-statement — Type (consolep leo-console-error-statement).

Definitions and Theorems

Function: j2f-console-error

(defun j2f-console-error (json-console-error)
 (declare (xargs :guard (json::memberp json-console-error)))
 (let ((__function__ 'j2f-console-error))
  (declare (ignorable __function__))
  (b*
   (((require-json-member-with-name json-console-error
                                    "Error" *error-console-error*))
    ((json::pattern
        (:object (:member "string" (:string litstring))
                 (:member "parameters"
                          (:array formatting-string-parameters..))))
     (json::member->value json-console-error))
    ((unless (and json::match? (stringp litstring)))
     (mv t *error-console-error*))
    ((mv erp leo-params)
     (j2f-expression-list formatting-string-parameters..))
    ((when erp)
     (mv t *error-console-error*)))
   (mv nil
       (make-console-error :string (acl2::explode litstring)
                           :exprs leo-params)))))