		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-struct-members

Converts a list of json struct members to a leo::compdecl-list.

Signature
(j2f-struct-members json-component-declarations) → (mv erp leo-component-declarations)
Arguments: json-component-declarations — Guard (json::value-listp json-component-declarations).
Returns: erp — Type (booleanp erp).; leo-component-declarations — Type (compdecl-listp leo-component-declarations).

Definitions and Theorems

Function: j2f-struct-members

(defun j2f-struct-members (json-component-declarations)
 (declare
     (xargs :guard (json::value-listp json-component-declarations)))
 (let ((__function__ 'j2f-struct-members))
   (declare (ignorable __function__))
   (b* (((when (endp json-component-declarations))
         (mv nil nil))
        (cdecl (first json-component-declarations))
        ((mv erp leo-cdecl)
         (j2f-struct-component-declaration cdecl))
        ((when erp) (mv t nil))
        ((mv erp rest-leo-cdecls)
         (j2f-struct-members (rest json-component-declarations)))
        ((when erp) (mv t nil)))
     (mv nil (cons leo-cdecl rest-leo-cdecls)))))