		Search-engine friendly clone of the ACL2 documentation.

Irr-binop

An irrelevant binary operator.

This can be used as a dummy value of the type.

Function: irr-binop

(defun irr-binop nil
  (declare (xargs :guard t))
  (binop-asg))

Theorem: binopp-of-irr-binop

(defthm binopp-of-irr-binop
  (b* ((acl2::irr (irr-binop)))
    (binopp acl2::irr))
  :rule-classes :rewrite)