Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Vwsim
Fgl
Vl
Syntax
Loader
Warnings
Getting-started
Utilities
Printer
Kit
Vl-lint
Vl-server
Vls-scannedalist-p
Vls-loadedalist-p
Vls-commands
Vls-data-p
Vl-server-opts-p
Vl-descriptionlist-summaries
Vls-transdb
Vl-describe
Ts-queue
Vls-get-plainsrc
Vl-description->warnings
Vls-showloc
File-layout
Vl-zipinfo
Vl-zipinfo-fix
Vl-zipinfo-equiv
Make-vl-zipinfo
Vl-zipinfo-p
Change-vl-zipinfo
Vl-zipinfo->syntax
Vl-zipinfo->filename
Vl-zipinfo->name
Vl-zipinfo->ltime
Vl-zipinfo->date
Vl-scan-for-zipinfos-aux
Vl-scan-for-zipinfos
Vl-zipinfolist
Vls-remove-from-scannedalist
Vls-describe
Vl-server-top
Vls-port-table
Vl-find-description-insensitive
Vls-get-warnings
Vls-get-summary
Vls-get-origsrc
Vl-ppc-description
Vls-get-parents
Vls-get-children
Vls-data-origname-reportcard
Vls-data-from-zip
Start
Vls-make-scannedalist
Vls-get-summaries
Vls-get-unloaded-json
Vls-get-desctypes
Vls-scannedalist-to-json
Vls-loadedalist-to-json
Vl-description-summary
*vl-server-help*
Vl-descalist->descriptions/types
Stop
Vl-gather
Vl-zip
Vl-main
Split-plusargs
Vl-shell
Vl-json
Mlib
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
File-layout
Vl-zipinfo
Meta information about .vlzip files we find.
This is a product type introduced by
defprod
.
Fields
filename —
stringp
Short filename of the vlzip file.
name —
stringp
Project name extracted from the vlzip file.
syntax —
stringp
Syntax version of this vlzip file.
date —
stringp
Human-friendly date stamp for this vlzip file.
ltime —
natp
Lisp time stamp (seconds since 1900) of this vlzip file.
Subtopics
Vl-zipinfo-fix
Fixing function for
vl-zipinfo
structures.
Vl-zipinfo-equiv
Basic equivalence relation for
vl-zipinfo
structures.
Make-vl-zipinfo
Basic constructor macro for
vl-zipinfo
structures.
Vl-zipinfo-p
Recognizer for
vl-zipinfo
structures.
Change-vl-zipinfo
Modifying constructor for
vl-zipinfo
structures.
Vl-zipinfo->syntax
Get the
syntax
field from a
vl-zipinfo
.
Vl-zipinfo->filename
Get the
filename
field from a
vl-zipinfo
.
Vl-zipinfo->name
Get the
name
field from a
vl-zipinfo
.
Vl-zipinfo->ltime
Get the
ltime
field from a
vl-zipinfo
.
Vl-zipinfo->date
Get the
date
field from a
vl-zipinfo
.