Extensional equality (=~= and =~~=)

The shallow extensional equality operator =~= and deep extensional equality operator =~~= are both equivalent to spec equality (==).

These operators are distinguished only by their impact on the proof search. Specifically, the use of the =~= and =~~= operators will trigger the application of “extensional equality” operators.

See the guide page for an introductory explanation with motivation.

Syntax

ext_eq_expr ::= spec_expr =~=  spec_expr
              | spec_expr =~~= spec_expr

Typing

The extensional equality operator requires both the left-hand side and right-hand side to have the same type. The expression returns a bool.

Semantics

The operator is equivalent to spec equality.