test(tests/lean): move simp_loop test to slow subdirectory

This example produces a stackoverflow on Valgrind.
We don't execute Valgrind on tests in the slow subdirectory.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean): use ascii prefix for auxiliary let-declarations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/simplifier): must use metavar_env in is_ceq, otherwise it may ceqs that contain metavariables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/simplifier): discard conditional equations that are clearly non-terminating

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean): new simplifier test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/simplifier): check if the given types are convertible to ceq expected types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): make the parser accept (Type -> ...)

Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): make the parser accept (Type -> ...)