• 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-command-args-to-eformals
              • Vls-commandinfo-p
                • Vls-commandinfo
                • Make-vls-commandinfo
                • Change-vls-commandinfo
                • Make-honsed-vls-commandinfo
                • Honsed-vls-commandinfo
                • Vls-commandinfo->type
                • Vls-commandinfo->fn
                • Vls-commandinfo->args
              • Vls-success
              • Vls-commandinfolist-p
              • Commands-table
              • Define-vls-command-fn
              • Vls-fail-fn
              • Vls-fail
              • Vls-command-arg-to-eformal
              • Vls-commandtype-p
              • Get-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
            • 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
  • Vls-commands

Vls-commandinfo-p

(vls-commandinfo-p x) is a defaggregate of the following fields.

  • fn — Name of the function that will execute this command. Should have the signature (fn [args] data) → string.
        Invariant (symbolp fn).
  • args — Names of the arguments.
        Invariant (symbol-listp args).
  • type — Content type produced by this command.
        Invariant (vls-commandtype-p type).

Source link: vls-commandinfo-p

Subtopics

Vls-commandinfo
Raw constructor for vls-commandinfo-p structures.
Make-vls-commandinfo
Constructor macro for vls-commandinfo-p structures.
Change-vls-commandinfo
A copying macro that lets you create new vls-commandinfo-p structures, based on existing structures.
Make-honsed-vls-commandinfo
Constructor macro for honsed vls-commandinfo-p structures.
Honsed-vls-commandinfo
Raw constructor for honsed vls-commandinfo-p structures.
Vls-commandinfo->type
Access the type field of a vls-commandinfo-p structure.
Vls-commandinfo->fn
Access the fn field of a vls-commandinfo-p structure.
Vls-commandinfo->args
Access the args field of a vls-commandinfo-p structure.