It now performs self simplification, and the performance is slightly better. As described at issue #1675, only non dependent propositions are considered. @Armael: this tactic may be useful for you |
||
|---|---|---|
| .. | ||
| data | ||
| init | ||
| smt | ||
| system | ||
| tools/debugger | ||
| leanpkg.path | ||
| library.md | ||
| standard.lean | ||