|
|
|---|
|
|
|
|---|
Leo equality operations.
Here we mean both equality
Each of these operations is defined on all Leo values, but the two operands must have the same type. That is, it is not possible to compare for (in)equality two Leo values of different types, even though they could be simply considered not equal. But requiring the same type promotes better programming discipline.
We model these two operations via two ACL2 functions that return a Leo boolean value when both arguments have the same type. If they have different types, we defensively return an error. If they have the same type, we just use ACL2's equal: this is correct because our current model of values has a unique representation for each value.