• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
        • 4v-sexprs
          • 4v-sexpr-vars
            • 4v-sexpr-vars-1pass
            • 4v-nsexpr-vars
            • 4v-sexpr-vars-1pass-list-list
            • 4v-sexpr-vars-list-list
            • 4v-sexpr-vars-alists
            • 4v-sexpr-vars-alist
            • 4v-sexpr-vars-1pass-list
            • 4v-sexpr-vars-list
            • 4v-sexpr-eval
            • 4v-sexpr-to-faig
            • 4v-sexpr-restrict-with-rw
            • 4vs-constructors
            • 4v-sexpr-compose-with-rw
            • 4v-sexpr-restrict
            • 4v-sexpr-alist-extract
            • 4v-sexpr-compose
            • 4v-nsexpr-p
            • 4v-sexpr-purebool-p
            • 4v-sexpr-<=
            • Sfaig
            • Sexpr-equivs
            • 3v-syntax-sexprp
            • Sexpr-rewriting
            • 4v-sexpr-ind
            • 4v-alist-extract
          • 4v-monotonicity
          • 4v-operations
          • Why-4v-logic
          • 4v-<=
          • 4vp
          • 4vcases
          • 4v-fix
          • 4v-lookup
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • 4v-sexpr-vars

    4v-sexpr-vars-list

    Extension of 4v-sexpr-vars to a sexpr list.

    (4v-sexpr-vars-list x) is is the mutually recursive counterpart of 4v-sexpr-vars. It is given a list of sexprs, and returns a single set containing all the variables in these sexprs.