|
|
|---|
|
|
|
|---|
Leo logical operations.
These are conjunction, disjunction, negated conjunction, and negated disjunction. They are all binary.
There is also a unary logical operation, op-not, that is allowed on both boolean and integer values.
The operations here are only allowed on boolean values. We formalize them via ACL2 functions over all Leo values, defined so that they return an error on non-boolean values. This is part of our defensive definition of the Leo dynamic semantics, in which attempts to apply operations on operands of the wrong type result in errors.