		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-console-assert

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

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

Definitions and Theorems

Function: j2f-console-assert

(defun j2f-console-assert (json-console-assert)
 (declare (xargs :guard (json::memberp json-console-assert)))
 (let ((__function__ 'j2f-console-assert))
  (declare (ignorable __function__))
  (b* (((require-json-member-with-name
             json-console-assert
             "Assert" *error-console-assert*))
       (jc-assert-value (json::member->value json-console-assert))
       ((mv erp leo-console-assert-expression)
        (j2f-expression jc-assert-value)))
    (mv erp
        (make-console-assert :arg leo-console-assert-expression)))))