Remark: this is just the first step, we still need to populate the `conv.interactive` namespace with tactics such as rewrite, simp, etc. |
||
|---|---|---|
| .. | ||
| data | ||
| init | ||
| smt | ||
| system | ||
| tools/debugger | ||
| leanpkg.path | ||
| library.md | ||
| standard.lean | ||
Remark: this is just the first step, we still need to populate the `conv.interactive` namespace with tactics such as rewrite, simp, etc. |
||
|---|---|---|
| .. | ||
| data | ||
| init | ||
| smt | ||
| system | ||
| tools/debugger | ||
| leanpkg.path | ||
| library.md | ||
| standard.lean | ||