		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-funinputs

Converts a list of json fn input parameters to a leo::funinput-list.

Signature
(j2f-funinputs json-fn-inputs) → (mv erp leo-inputs)
Arguments: json-fn-inputs — Guard (json::value-listp json-fn-inputs).
Returns: erp — Type (booleanp erp).; leo-inputs — Type (funinput-listp leo-inputs).

Definitions and Theorems

Function: j2f-funinputs

(defun j2f-funinputs (json-fn-inputs)
  (declare (xargs :guard (json::value-listp json-fn-inputs)))
  (let ((__function__ 'j2f-funinputs))
    (declare (ignorable __function__))
    (b* (((when (endp json-fn-inputs))
          (mv nil nil))
         (inp (first json-fn-inputs))
         ((mv erp leo-fn-input)
          (j2f-outer-funinput inp))
         ((when erp) (mv t nil))
         ((mv erp rest-leo-fn-inputs)
          (j2f-funinputs (rest json-fn-inputs)))
         ((when erp) (mv t nil)))
      (mv nil
          (cons leo-fn-input rest-leo-fn-inputs)))))