Leonardo de Moura
|
e17ba27596
|
fix(library/tactic/rewrite_tactic): adjust the behavior of class resolution in rewriter
The solution is not very satisfactory. I should investigate it more.
|
2015-02-05 19:08:47 -08:00 |
|
Leonardo de Moura
|
96c161a659
|
feat(library/algebra/ring): simplify ring theorems using rewrite tactic
|
2015-02-05 18:48:02 -08:00 |
|
Leonardo de Moura
|
0ae6e2b3e4
|
feat(library/algebra/group): use rewrite tactic in the algebraic hierarchy
|
2015-02-05 18:03:02 -08:00 |
|
Leonardo de Moura
|
e097977bac
|
test(tests/lean/run): add more rewrite tactic tests
|
2015-02-05 14:09:07 -08:00 |
|
Leonardo de Moura
|
ffe0d1186e
|
feat(library/tactic/rewrite_tactic): add "reduce_to" step at rewrite tactic
|
2015-02-05 13:59:55 -08:00 |
|
Leonardo de Moura
|
116c65bff5
|
feat(library/tactic/rewrite_tactic): add reduction step to rewrite tactic
|
2015-02-05 13:42:50 -08:00 |
|
Leonardo de Moura
|
38ab4e7b3a
|
feat(frontends/lean/parse_rewrite_tactic): extend rewrite tactic parser
Add support for reduction steps.
|
2015-02-05 13:24:37 -08:00 |
|
Leonardo de Moura
|
7cdc88701d
|
feat(library/tactic/rewrite_tactic): add "reduction" step to rewrite tactic
|
2015-02-05 13:16:05 -08:00 |
|
Leonardo de Moura
|
808521223b
|
feat(library/tactic/rewrite_tactic): support constant unfolding in rewrite tactic
|
2015-02-05 12:58:30 -08:00 |
|
Leonardo de Moura
|
5443609845
|
fix(frontends/lean/parse_rewrite_tactic): take namespaces into account when parsing constant to unfold
|
2015-02-05 12:41:11 -08:00 |
|
Leonardo de Moura
|
1b73764ad3
|
fix(tests/lean/run/elim2): adjust test to reflect recent changes
|
2015-02-05 10:54:00 -08:00 |
|
Leonardo de Moura
|
d6958be7e7
|
fix(library/tactic/location): replace cache must not be used when only a subset of all occurrences should be replaced at replace_occurrences
|
2015-02-05 10:50:40 -08:00 |
|
Leonardo de Moura
|
bc8bb1dbd3
|
feat(kernel/replace_fn): add use_cache flag to replace function
|
2015-02-05 10:49:18 -08:00 |
|
Leonardo de Moura
|
2ffdbba8b0
|
feat(library): replace same 'calc' proofs with 'rewrite'
|
2015-02-05 10:39:25 -08:00 |
|
Leonardo de Moura
|
b6dd1269b9
|
feat(frontends/lean/builtin_exprs): make 'obtain' arguments visible by default
|
2015-02-05 10:38:45 -08:00 |
|
Leonardo de Moura
|
dfad24e3f5
|
feat(frontends/lean): polish rewrite tactic notation
|
2015-02-05 10:15:58 -08:00 |
|
Leonardo de Moura
|
941b493835
|
chore(library/tactic/rewrite_tactic): modify param name
|
2015-02-05 10:04:03 -08:00 |
|
Leonardo de Moura
|
0abfa30ead
|
fix(library/tactic/rewrite_tactic): elaboration bug in the rewrite tactic steps/elements
|
2015-02-05 10:01:18 -08:00 |
|
Leonardo de Moura
|
15efadfbdc
|
feat(frontends/lean/parse_rewrite_tactic): cleanup rewrite tactic notation
Make a rewrite command sequence explicit.
|
2015-02-04 20:16:24 -08:00 |
|
Leonardo de Moura
|
14c72e82f6
|
feat(library/tactic/rewrite_tactic): add support for rewriting hypotheses
|
2015-02-04 20:04:19 -08:00 |
|
Leonardo de Moura
|
90eb5c8ca5
|
test(tests/lean/hott): add test for rewriter in the HoTT version
|
2015-02-04 19:33:08 -08:00 |
|
Leonardo de Moura
|
61a029d9df
|
fix(tests/lean/rewrite_loop): notation
|
2015-02-04 19:21:26 -08:00 |
|
Leonardo de Moura
|
d0171ffe7a
|
test(tests/lean/run): add more rewrite tactic examples
|
2015-02-04 19:19:46 -08:00 |
|
Leonardo de Moura
|
08dcc9e2fc
|
feat(frontends/lean/parse_rewrite_tactic): polish rewrite tactic notation
|
2015-02-04 19:19:19 -08:00 |
|
Leonardo de Moura
|
55fb678db2
|
fix(library/tactic/location): clang++ 3.3 compilation problem
|
2015-02-04 18:48:23 -08:00 |
|
Leonardo de Moura
|
42c2f7eb11
|
fix(library/tactic/rewrite_tactic): memory leak
|
2015-02-04 18:40:11 -08:00 |
|
Leonardo de Moura
|
89fde9d829
|
feat(library/tactic/rewrite_tactic): add maximum number of iterations threshold to rewrite tactic
The idea is to avoid nontermination.
|
2015-02-04 16:13:15 -08:00 |
|
Soonho Kong
|
ca16381892
|
feat(bin): add linja.in and LEAN_BIN_DEP cmake option
see the discussion in issue #422
|
2015-02-04 15:46:08 -08:00 |
|
Leonardo de Moura
|
dc297865d4
|
chore(library/tactic/rewrite_tactic): fix compilation warnings
|
2015-02-04 15:34:02 -08:00 |
|
Leonardo de Moura
|
0c8eaa38c8
|
test(tests/lean/run): add basic rewriter test
|
2015-02-04 15:30:18 -08:00 |
|
Leonardo de Moura
|
ee079d12f4
|
feat(library/tactic/rewrite_tactic): remove trivial goal in rewrite_tactic
|
2015-02-04 15:29:52 -08:00 |
|
Leonardo de Moura
|
f0fac1ae0e
|
feat(library/constants): add eq.intro
|
2015-02-04 15:27:18 -08:00 |
|
Leonardo de Moura
|
e5381679d6
|
feat(library/tactic/rewrite_tactic): rewrite goal
|
2015-02-04 15:17:58 -08:00 |
|
Leonardo de Moura
|
599de0271b
|
feat(frontends/lean/parse_tactic_location): validate occurrence index
|
2015-02-04 14:04:56 -08:00 |
|
Leonardo de Moura
|
09818adf90
|
feat(library/tactic/rewrite_tactic): elaborate rewrite rule using unifier
|
2015-02-04 13:51:32 -08:00 |
|
Leonardo de Moura
|
49323ab598
|
feat(library/util): add mk_symm
|
2015-02-04 13:44:55 -08:00 |
|
Leonardo de Moura
|
ccae014ef9
|
feat(library/tactic/rewrite_tactic): ignore inst_implicit arguments when matching applications of declarations which contain them
|
2015-02-04 12:14:47 -08:00 |
|
Leonardo de Moura
|
0e05c239a5
|
feat(library/tactic/rewrite_tactic): add custom matcher pluging for rewriter
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
8912c759dd
|
fix(frontends/lean/parse_rewrite_tactic): corner case "rewrite ?(t)"
The token '?(' is used to represent inaccessible terms in recursive
equations. In the rewriter tactic, we want "rewrite ?(t)" to be parsed
as "? (t)".
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
991d29b7f6
|
fix(frontends/lean/parse_rewrite_tactic): bugs in rewrite tactic parser
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
d6a7ec4621
|
chore(library/tactic/rewrite_tactic): fix style
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
b4dd2cc729
|
refactor(library/tactic/rewrite_tactic): more general rewrite step
The rule can be an arbitrary expression.
Allow user to provide a pattern that restricts the application of the rule.
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
461fd45efc
|
feat(frontends/lean): allow a different location for each rewrite element
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
c845e44777
|
feat(frontends/lean): parse rewrite tactic
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
180cda304e
|
feat(library/tactic): add rewrite tactic skeleton
The tactic has not been implemented yet, but this commit adds all the
support for storing arguments, serializing and deserializing them.
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
87bcec2e5e
|
feat(frontends/lean): parse tactic location (i.e., scope of application)
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
8a78adc9af
|
feat(library/tactic): add auxiliary object "location"
This object will used to specify the scope of application of tactics
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
2a6ccb252e
|
test(tests/lean/extra): add regression tests for issue #422
|
2015-02-04 10:55:03 -08:00 |
|
Leonardo de Moura
|
0cea63651d
|
fix(frontends/lean): store line/col information at snapshots, save snapshot before 'end' scope, and before "closing" open namespaces
closes #422
|
2015-02-04 10:40:36 -08:00 |
|
Leonardo de Moura
|
420da8fd3f
|
feat(library/projection): store bit saying whether a projection is for a class or not.
|
2015-02-04 08:54:20 -08:00 |
|