		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vls-loadedalist-to-json

Signature
(vls-loadedalist-to-json x) → *
Arguments: x — Guard (vls-loadedalist-p x).

Definitions and Theorems

Function: vls-loadedalist-to-json

(defun vls-loadedalist-to-json (x)
  (declare (xargs :guard (vls-loadedalist-p x)))
  (let ((__function__ 'vls-loadedalist-to-json))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((cons name (vls-data data)) (car x))
         (entry (list (cons "name" data.name)
                      (cons "date" data.date)
                      (cons "ltime" data.ltime)
                      (cons "compat" t))))
      (cons (cons name entry)
            (vls-loadedalist-to-json (cdr x))))))