Open GoogleCodeExporter opened 9 years ago
Also, having let definition should trigger the simplification stuff and that
could be helpful.
Original comment by pedag...@gmail.com
on 7 Sep 2010 at 11:21
The problem here is that we get a lot less propositional simplification when
using 'let': we don't look for recursive calls when searching for proofs, and
we don't simplify propositions in programming problem goals. The former should
not be very hard to implement, but I'm not sure when we want the latter.
Original comment by adamgundry
on 7 Sep 2010 at 11:36
Original issue reported on code.google.com by
pedag...@gmail.com
on 7 Sep 2010 at 11:19