		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vls-scannedalist-to-json

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

Definitions and Theorems

Function: vls-scannedalist-to-json

(defun vls-scannedalist-to-json (x)
  (declare (xargs :guard (vls-scannedalist-p x)))
  (let ((__function__ 'vls-scannedalist-to-json))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((cons name (vl-zipinfo info)) (car x))
         (entry (list (cons "name" info.name)
                      (cons "date" info.date)
                      (cons "ltime" info.ltime)
                      (cons "compat"
                            (equal info.syntax
                                   *vl-current-syntax-version*)))))
      (cons (cons name entry)
            (vls-scannedalist-to-json (cdr x))))))