| Source File | Identifier index | Theory binding index |
|---|
signature NumRelNorms =
sig
include Abbrev
val ADDL_CANON_CONV : conv
val ADDR_CANON_CONV : conv
val MUL_CANON_CONV : conv
(* these three normalise relational expressions of the form
e1 <relop> e2
taking, for example with sum_eq_norm,
x + (y + 7) = x + 10
to
y = 3
They all assume that both expressions have already been canonicalised
with ADDR_CANON_CONV
*)
val sum_leq_norm : conv
val sum_lt_norm : conv
val sum_eq_norm : conv
end
| Source File | Identifier index | Theory binding index |
|---|