feat(library/simplifier): add support for 'permutation' rewrite rules

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/expr): add efficient get_size() function for expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/expr_lt): make sure the total order on terms is monotonic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/expr): compilation warning

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/simplifier): ordered rewriting

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/library/expr_lt): adjust is_lt unit tests to reflect recent modifications

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/expr): make sure semantic attachments are smaller than other kinds of expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(*): semantic attachment parsing and simplification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean): adjust test to reflect recent changes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin/Nat): flip orientation of associativity axioms for + and *

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin/Nat): flip orientation of associativity axioms for + and *