• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
          • Defstv
          • Stv-compile
          • Symbolic-test-vector-format
          • Stv-implementation-details
          • Compiled-stv-p
          • Stv-run-for-all-dontcares
          • Stv-run
          • Stv-process
          • Stv-run-check-dontcares
          • Symbolic-test-vector-composition
          • Stv-expand
          • Stv-easy-bindings
            • Stv-easy-bindings-inside-mix
            • Stv-debug
            • Stv-run-squash-dontcares
            • Stvdata-p
            • Stv-doc
            • Stv2c
            • Stv-widen
            • Stv-out->width
            • Stv-in->width
            • Stv-number-of-phases
            • Stv->outs
            • Stv->ins
            • Stv-suffix-signals
            • Stv->vars
          • Esim-primitives
          • E-conversion
          • Esim-steps
          • Patterns
          • Mod-internal-paths
          • Defmodules
          • Esim-simplify-update-fns
          • Esim-tutorial
          • Esim-vl
        • Vl2014
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Stv-easy-bindings

    Stv-easy-bindings-inside-mix

    Signature
    (stv-easy-bindings-inside-mix x stv) → *
    Arguments
    x — Some arguments inside of a :mix.
    stv — Guard (processed-stv-p stv).

    Definitions and Theorems

    Function: stv-easy-bindings-inside-mix

    (defun stv-easy-bindings-inside-mix (x stv)
     (declare (xargs :guard (processed-stv-p stv)))
     (let ((__function__ 'stv-easy-bindings-inside-mix))
      (declare (ignorable __function__))
      (cond
       ((atom x) nil)
       ((symbolp (car x))
        (cons (cons ':nat
                    (cons (car x)
                          (cons (stv-in->width (car x) stv)
                                'nil)))
              (stv-easy-bindings-inside-mix (cdr x)
                                            stv)))
       (t
        (raise
         "Inside a :mix you can only have symbols (the names of stv ~
                     inputs), so ~x0 is illegal."
         (car x))))))