		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-let-or-const-statement

Converts a json-member let statement to a leo::statmement of kind :let.

Signature
(j2f-let-or-const-statement json-let-or-const-statement) → (mv erp leo-let-or-const-statement)
Arguments: json-let-or-const-statement — Guard (json::memberp json-let-or-const-statement).
Returns: erp — Type (booleanp erp).; leo-let-or-const-statement — Type (statementp leo-let-or-const-statement).

Definitions and Theorems

Function: j2f-let-or-const-statement

(defun j2f-let-or-const-statement (json-let-or-const-statement)
 (declare
      (xargs :guard (json::memberp json-let-or-const-statement)))
 (let ((__function__ 'j2f-let-or-const-statement))
  (declare (ignorable __function__))
  (b*
   (((unless
      (and
          (json::memberp json-let-or-const-statement)
          (equal "Definition"
                 (json::member->name json-let-or-const-statement))))
     (mv t *error-let-statement*))
    (def-member-val
         (json::member->value json-let-or-const-statement))
    ((json::pattern (:object (:member "declaration_type"
                                      (:string let-or-const))
                             *..))
     def-member-val)
    ((unless (and json::match?
                  (member-equal let-or-const '("Let" "Const"))))
     (mv t *error-let-statement*)))
   (if (equal let-or-const "Let")
       (j2f-let-statement def-member-val)
     (j2f-const-statement def-member-val)))))