• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
          • 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
          • Vl-descriptionlist-summaries
          • Vls-transdb
          • File-layout
          • Vls-data-p
          • Ts-queue
          • Vls-showloc
          • Vls-get-plainsrc
          • Vl-description->warnings
          • Vl-describe
          • Vls-port-table
          • Vls-describe
          • Vls-data-from-translation
          • Vl-find-description-insensitive
          • Vls-get-warnings
          • Vls-get-summary
          • Vls-get-origsrc
          • Vls-data-origname-reportcard
          • Vls-get-parents
          • Vls-get-children
          • Vls-get-summaries
          • Vl-ppc-description
          • Vls-get-desctypes
          • Vl-description-summary
          • Start
          • Vl-descalist->descriptions/types
          • Stop
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • 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.