2 commits

Author	SHA1	Message	Date
Leonardo de Moura	a9515ac7a4	feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function ... See issue #692. The implementation still has some rough spots. It is not clear what the right semantic is. Moreover, the folds in e_closure could not be eliminated automatically.	2015-07-08 21:19:18 -04:00
Leonardo de Moura	5b25da8c43	feat(frontends/lean): add esimp tactic based on rewrite tactic ... closes #358	2015-02-06 14:13:32 -08:00