Equivalence Relation¶
Syntax¶
syntax cmpexpr
{
x[scomparison_pri]:= x[>scomparison_pri] cmp x[>scomparison_pri] =># "`(ast_apply ,_sr (,_2 (,_1 ,_3)))";
x[scomparison_pri]:= x[>scomparison_pri] "not" cmp x[>scomparison_pri] =># "`(ast_not ,_sr (ast_apply ,_sr (,_3 (,_1 ,_4))))";
cmp := "==" =># "(nos _1)";
cmp := "!=" =># "(nos _1)";
cmp := "\ne" =># '(nos _1)';
cmp := "\neq" =># '(nos _1)';
}
Semantics¶
class Eq[t] {
virtual fun == : t * t -> bool;
virtual fun != (x:t,y:t):bool => not (x == y);
axiom reflex(x:t): x == x;
axiom sym(x:t, y:t): (x == y) == (y == x);
axiom trans(x:t, y:t, z:t): x == y and y == z implies x == z;
fun eq(x:t, y:t)=> x == y;
fun ne(x:t, y:t)=> x != y;
fun \ne(x:t, y:t)=> x != y;
fun \neq(x:t, y:t)=> x != y;
}