Four-valued semantics for a pullup resistor.
(4v-pullup a) acts just like a buffer except that, if its input is floating, it instead produces true. That is, it returns the value specified by the following truth table:
a | out -----+------- F | F T | T X | X Z | T
(defun 4v-pullup (a) (declare (xargs :guard t)) (4vcases a (t (4vt)) (z (4vt)) (f (4vf)) (& (4vx))))