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>
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.