Parse decimal values

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add 'Variables' command.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add (optional) type to let declarations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix bug in the elaborator. Move character ' to class A

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add missing case to elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix problem with pretty printer. Add another test for elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Improve check_pi in lean elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add casting propagation and normalization

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add castlib as an independent library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Move Symm and Trans back to basic_thms.cpp

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add examples that demonstrate limitations of the current elaborator. The new design, we are working on, will be able to solve them.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Improve pretty printer for Pi's

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces)

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

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