Leonardo de Moura
|
093a212ed4
|
test(tests/lean/run/blast21): another blast test
|
2015-11-18 19:20:32 -08:00 |
|
Leonardo de Moura
|
3bd83b8e41
|
feat(library/blast/backward/backward_strategy): don't try constructor action by default
|
2015-11-18 19:14:37 -08:00 |
|
Leonardo de Moura
|
3f6ec66b36
|
test(tests/lean/run/blast20): more tests
|
2015-11-18 19:12:58 -08:00 |
|
Daniel Selsam
|
413989afd6
|
feat(library/blast/backward): backward chaining strategy
|
2015-11-18 17:48:39 -08:00 |
|
Leonardo de Moura
|
e580e6cdb1
|
fix(tests/lean/interactive/findp): adjust test
|
2015-11-18 10:10:46 -08:00 |
|
Leonardo de Moura
|
de67288305
|
fix(library/app_builder): mk_rel supports relations where the lhs and rhs are not necessarily the last two arguments (e.g., heq)
|
2015-11-17 18:45:22 -08:00 |
|
Leonardo de Moura
|
f363975856
|
feat(frontends/lean): add command #congr_rel for testing new congruence lemma for equivalence relations
|
2015-11-17 18:45:22 -08:00 |
|
Leonardo de Moura
|
a96aed6dfe
|
test(tests/lean): add tests for simp priorities
|
2015-11-16 22:41:04 -08:00 |
|
Leonardo de Moura
|
491c7c55e1
|
feat(library/simplifier/simp_rule_set): add priorities for simp and congr rules
|
2015-11-16 22:34:06 -08:00 |
|
Leonardo de Moura
|
5095f05303
|
fix(tests/lean/interactive/findp): adjust test to recent changes in the standard lib
|
2015-11-16 21:30:28 -08:00 |
|
Daniel Selsam
|
835e8995b4
|
test(simplifier19): nested fusion
|
2015-11-16 20:39:16 -08:00 |
|
Daniel Selsam
|
a689c66b1e
|
fix(library/blast/simplifier): handle scalar in fusion
|
2015-11-16 20:39:15 -08:00 |
|
Daniel Selsam
|
49ff8640d9
|
fix(library/blast/simplifier): use ac rules for numerals
|
2015-11-16 20:39:15 -08:00 |
|
Daniel Selsam
|
8ca5d87f0b
|
feat(library/blast/simplifier): rely on norm_num for recursion
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
7cd15aaecd
|
test(simplifier11): add necessary simp rule
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
6ba42bb7bc
|
test(simplifier11.lean): add rule for (not P)
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
a02459fe5e
|
test(simplifier9.lean): fix order of congr rules
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
b9a516783c
|
fix(library/blast/simplifier): remove unnecessary casts
|
2015-11-16 20:33:22 -08:00 |
|
Leonardo de Moura
|
60945e95b4
|
feat(library/blast): add 'discard' action for detecting irrelevant hypotheses
|
2015-11-16 11:43:51 -08:00 |
|
Leonardo de Moura
|
b3ca5faa49
|
fix(tests/lean): some of the simplifier tests
|
2015-11-16 11:01:53 -08:00 |
|
Daniel Selsam
|
5e8068b2b2
|
feat(library/blast/simplifier): draft of fusion
|
2015-11-16 09:13:07 -08:00 |
|
Daniel Selsam
|
6290919170
|
test(tests/lean/simplifier_norm_num): add moderate sized test
|
2015-11-16 09:13:07 -08:00 |
|
Daniel Selsam
|
30b1b79c4e
|
fix(algebra/simplifier): update numeral simp rules
|
2015-11-16 09:12:29 -08:00 |
|
Leonardo de Moura
|
db59c6829c
|
feat(library/blast): add basic support for non-recursive recursors/eliminators in the simple_strategy, fix bug at recursor_action
|
2015-11-15 18:39:12 -08:00 |
|
Leonardo de Moura
|
a545860aa1
|
feat(library/blast/intros_action): apply head_beta_reduce at intros
|
2015-11-15 18:14:12 -08:00 |
|
Leonardo de Moura
|
24ed427c2f
|
feat(library/blast): add "recursor" (aka elimination/induction) action
|
2015-11-15 18:00:32 -08:00 |
|
Leonardo de Moura
|
0dc31227f8
|
feat(library/init/logic): mark ne reducible
|
2015-11-15 15:09:02 -08:00 |
|
Leonardo de Moura
|
60434b3487
|
fix(tests/lean/urec): adjust test to recent changes
|
2015-11-15 15:06:05 -08:00 |
|
Leonardo de Moura
|
1308c7c4e2
|
feat(library/blast): add action for not(a ~ a) when ~ is a reflexive relation
|
2015-11-15 15:00:25 -08:00 |
|
Leonardo de Moura
|
ff73fb22fb
|
feat(library/user_recursors): store whether recursor is recursive or not
|
2015-11-15 12:37:35 -08:00 |
|
Leonardo de Moura
|
676ffb77f9
|
test(tests/lean/run): test for simp action
|
2015-11-15 11:36:24 -08:00 |
|
Leonardo de Moura
|
fd41a4f76d
|
feat(library/blast): add simplify_target action
|
2015-11-14 16:18:12 -08:00 |
|
Leonardo de Moura
|
b5db77961d
|
feat(library/blast): add "trivial" action
|
2015-11-14 15:02:14 -08:00 |
|
Leonardo de Moura
|
0f4e59a84f
|
feat(library/blast): add "no_confusion" action
|
2015-11-13 18:19:05 -08:00 |
|
Leonardo de Moura
|
29d472788f
|
feat(library/blast/subst): avoid unnecessary proof step
|
2015-11-13 16:31:07 -08:00 |
|
Leonardo de Moura
|
3849aff674
|
fix(library/blast/subst): bug in subst action, add hypothesis_idx_buffer_set (helper class), refine revert_action interface
|
2015-11-13 16:10:25 -08:00 |
|
Leonardo de Moura
|
65b962dabd
|
test(tests/lean/run): add basic tests for subst action
|
2015-11-13 15:27:54 -08:00 |
|
Leonardo de Moura
|
0316412992
|
test(tests/lean/simplifier_norm_num): disable test that is taking a long time
|
2015-11-13 09:25:39 -08:00 |
|
Daniel Selsam
|
00a5cd519e
|
feat(algebra/simplifier): simp rule set for units
|
2015-11-12 21:23:28 -08:00 |
|
Daniel Selsam
|
e7890fb456
|
feat(algebra/simplifier): useful simp rule sets
|
2015-11-12 21:23:28 -08:00 |
|
Daniel Selsam
|
f17320eccf
|
fix(library/abstract_expr_manager): remove weight and lt
|
2015-11-12 21:21:52 -08:00 |
|
Daniel Selsam
|
3703938e55
|
feat(library/abstract_expr_manager): compare exprs ignoring subsingletons
|
2015-11-12 21:21:51 -08:00 |
|
Leonardo de Moura
|
182085b366
|
fix(tests/lean/simplifier_norm_num): adjust tests to recent changes
|
2015-11-12 20:59:26 -08:00 |
|
Rob Lewis
|
44a099f6f1
|
feat(norm_num): performance and style fixes
|
2015-11-12 20:53:37 -08:00 |
|
Rob Lewis
|
4bf0519843
|
feat(norm_num): numeral normalizer works for +, -, *, /
|
2015-11-12 20:53:37 -08:00 |
|
Rob Lewis
|
616450be64
|
feat(library/norm_num): extend norm_num to handle subtraction
|
2015-11-12 20:53:37 -08:00 |
|
Leonardo de Moura
|
e1f81cfdcd
|
feat(library/type_context): add normalizer for type_context
|
2015-11-12 20:31:36 -08:00 |
|
Leonardo de Moura
|
9aaa2d0991
|
feat(frontends/lean): add new command for testing new congruence lemmas
Remark: #congr_simp is the old command, and #congr is the new one.
|
2015-11-12 18:55:25 -08:00 |
|
Leonardo de Moura
|
5ceac83b6a
|
feat(frontends/lean/elaborator): restrict the number of places where coercions are considered
We do not consider coercions around meta-variables anymore.
|
2015-11-11 12:37:19 -08:00 |
|
Leonardo de Moura
|
296a4ab940
|
test(tests/lean/run): add coercion test issue
|
2015-11-11 12:12:15 -08:00 |
|