		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-function-definitions

Converts list of json-members, all of which are supposed to be functions, to a list of leo::definitions.

Signature
(j2f-function-definitions json-fns) → (mv erp leo-function-definitions)
Arguments: json-fns — Guard (json::member-listp json-fns).
Returns: erp — Type (booleanp erp).; leo-function-definitions — Type (definition-listp leo-function-definitions).

Definitions and Theorems

Function: j2f-function-definitions

(defun j2f-function-definitions (json-fns)
  (declare (xargs :guard (json::member-listp json-fns)))
  (let ((__function__ 'j2f-function-definitions))
    (declare (ignorable __function__))
    (if (endp json-fns)
        (mv nil nil)
      (b* ((first-json-fn (first json-fns))
           ((mv erp first-leo-fn)
            (j2f-function-definition-not-test first-json-fn))
           ((when erp)
            (mv erp (list first-leo-fn)))
           (rest-json-fns (rest json-fns))
           ((mv erp rest-leo-fns)
            (j2f-function-definitions rest-json-fns))
           ((when erp) (mv erp rest-leo-fns)))
        (mv nil
            (cons first-leo-fn rest-leo-fns))))))