Leonardo de Moura
6208934134
feat(library/init/meta/converter/interactive): add support for rw at conv tactical
2017-06-30 12:41:35 -07:00
Leonardo de Moura
f7fe2a775c
feat(library/init/meta/rewrite_tactic): improve rewrite tactic
...
`rewrite` tactic improvements
- Add support for `auto_param` and `opt_param`
- Order new goals using the same strategies available for `apply`
- Allow user to set configuration object in interactive mode.
@Armael This commit should address the issue you raised about the order
of new goals in the `rewrite` tactic.
See new test tests/lean/run/rw1.lean for examples.
2017-06-30 12:03:27 -07:00
Leonardo de Moura
e1c76578c1
chore(tests/lean/run, doc/changes): more tests and document new feature
2017-06-29 17:12:04 -07:00
Leonardo de Moura
eb838c78bf
doc(changes): simp improvement
2017-06-28 18:29:44 -07:00
Sebastian Ullrich
16fe494736
feat(frontends/lean/scanner): accept arbitrary escaped identifiers
2017-06-28 10:43:19 -07:00
Leonardo de Moura
98ba6666dc
doc(changes): apply tactic
...
closes #1342
2017-06-27 18:44:54 -07:00
Sebastian Ullrich
46873d32ae
chore(doc/changes): update changelog
2017-06-27 22:08:45 +02:00
Leonardo de Moura
d666742219
doc(changes): update
2017-06-22 08:07:25 -07:00
Leonardo de Moura
14d768ffa2
feat(library/init/meta/interactive): add simp_all tactic
...
@Armael I added the simp_all tactic. See new test for an example.
2017-06-21 20:43:56 -07:00
Leonardo de Moura
058d073cba
feat(library/init/meta/interactive): allow user to write rw [f] to rewrite using the equational lemmas for f
...
The tactic succeeds if the expression can be rewritten using one of the
equational lemmas associated with `f`.
See discussion at #1680
2017-06-21 18:56:18 -07:00
Leonardo de Moura
b9dee04fdb
feat(library/tactic/simplify): add single_pass simplifier option (default is false)
2017-06-21 16:41:54 -07:00
Sebastian Ullrich
565e583915
chore(doc/changes): fix link
2017-06-21 13:23:02 -07:00
Sebastian Ullrich
676e8eee6c
chore(doc/changes): update changelog
2017-06-21 13:22:47 -07:00
Leonardo de Moura
1fb6c5b211
doc(changes): update
2017-06-19 11:24:17 -07:00
Leonardo de Moura
75ec32de94
doc(changes): has_repr and has_to_string
2017-06-18 18:40:29 -07:00
Leonardo de Moura
3ea5ac4340
chore(*): update change log, and bump work in progress version to 3.2.1
2017-06-18 11:15:09 -07:00
Sebastian Ullrich
d994da97c1
chore(doc/changes): fix link
2017-06-16 16:17:25 +02:00
Leonardo de Moura
7b69d829c3
doc(changes): add hole command feature
2017-06-15 07:40:19 -07:00
Leonardo de Moura
bce1f10ae4
doc(doc/changes): add missing features/changes
2017-06-14 23:12:18 -07:00
Jeremy Avigad
a045b0f00c
feat(doc/changes.md): create change log
2017-06-14 22:42:08 -07:00
