Fix missing case in the elaborator

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix type checker for let expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix elaborator for let-expressions

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Handle (and pretty print) elaborator error messages in the lean default frontend

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Improve elaborator interface. Now, the metavariables are created inside the elaborator. The elaborator-user only needs to create placeholders. Motivaton: the placeholders are meaningful independently of the elaborator. On the other hand, the metavariables depend on the elaborator state.

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

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Move files in examples directory to tests directory. They are not real examples

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add a real example. Fix bug in the parser

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Make sure we have unlimited stack space for testing the scripts

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