Fix typos

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Refactor elaborator for supporting overloads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Minimize use the colors in tests. The colors make the diff hard to read

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add support for overloads in the elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remove unnecessary files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add functions for 'updating expressions'. The new functions are used to simplify the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add coercion declarations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Move elaborator to lean default frontend. It is getting too specific

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add coercion support in the elaborator and pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Rename normalize and type_check to normalizer and type_checker (using a consistent naming convention)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Replace macros TypeM, TypeU, Int, Bool, True and False with constant global expressions. The macros were producing counterintuitive behavior. For example, we had an enumeration type with an element called Int.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remove virtual method kind from value class and subclasses. We can use dynamic_cast to achieve the same goal

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Metavariables will not be part of the kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add natural numbers. Fix how coercions and overloads interact (switch to approach used in C++). Add notation for natural and integer arithmetic. Rename m and u universe variables to M and U.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Modify verbose message for Set command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>