bool_EQ_CONV

Conv.bool_EQ_CONV : conv

Simplifies expressions involving boolean equality.

The conversion bool_EQ_CONV simplifies equations of the form t1 = t2, where t1 and t2 are of type bool. When applied to a term of the form t = t, the conversion bool_EQ_CONV returns the theorem

   |- (t = t) = T

When applied to a term of the form t = T, the conversion returns

   |- (t = T) = t

And when applied to a term of the form T = t, it returns

   |- (T = t) = t

Failure

Fails unless applied to a term of the form t1 = t2, where t1 and t2 are boolean, and either t1 and t2 are syntactically identical terms or one of t1 and t2 is the constant T.

Example

- bool_EQ_CONV (Parse.Term `T = F`);
val it = |- (T = F) = F : thm

- bool_EQ_CONV (Parse.Term `(0 < n) = T`);
val it = |- (0 < n = T) = 0 < n : thm