2.7.11.1 Compare

A function that performs comparison has a the following very simple virtual code representation.

T19

[[compare]] = (nil,nil)

The proof of theorem T19 is that the standard silly prelude contains the declaration compare = (nil,nil). Code in this form has the following semantics.

P17

For distinct trees x and y, [[compare]] (x,y) = nil

P18

[[compare]] (x,x) = (nil,nil)

In other words, the virtual code (nil,nil) implements a function that takes a pair of trees and returns true if and only if they are equal.

It would be fairly simple to write an equivalent virtual code application that implements this function if it were not realizable in this form by definition of the operator. However, this method is preferable because it saves space in virtual code and has a highly optimized implementation in C.