Leonardo de Moura
|
564e8f947d
|
refactor(library): cleanup
|
2015-11-22 14:10:02 -08:00 |
|
Leonardo de Moura
|
6fc0e41439
|
fix(library/blast/congruence_closure): proof generation for congruences such as (a = b) <-> (b = a)
The congruence closure module treats these two terms as the same thing.
So, we should take this into account when building proofs
|
2015-11-21 19:50:59 -08:00 |
|
Leonardo de Moura
|
5e9914ef45
|
feat(library/blast/congruence_closure): avoid eq.rec if major premise is eq.refl
|
2015-11-21 19:00:16 -08:00 |
|
Leonardo de Moura
|
607552e51f
|
feat(library/blast): add target_updated event
|
2015-11-21 17:58:21 -08:00 |
|
Leonardo de Moura
|
091b0f0cc7
|
feat(library/blast): add option for disabling congruence closure
|
2015-11-21 17:45:25 -08:00 |
|
Leonardo de Moura
|
c4328aad3a
|
feat(library/blast/congruence_closure): missing case
|
2015-11-21 17:40:15 -08:00 |
|
Leonardo de Moura
|
962a61801e
|
test(tests/lean/run/blast_cc8): add card based on finite_set test for congruence closure module
|
2015-11-21 15:04:16 -08:00 |
|
Leonardo de Moura
|
c49caf3740
|
feat(library/blast/congruence_closure): add support for user-defined congruence lemmas in the congruence closure module
|
2015-11-21 14:43:51 -08:00 |
|
Leonardo de Moura
|
a61869ba1a
|
feat(library/blast): add option for disabling simplifier
|
2015-11-21 12:19:55 -08:00 |
|
Leonardo de Moura
|
c280ddb2b0
|
fix(tests,doc): adjust tests and documentation
|
2015-11-20 17:03:17 -08:00 |
|
Leonardo de Moura
|
85601c5a83
|
chore(library/blast/congruence_closure): fix style
|
2015-11-20 16:46:28 -08:00 |
|
Leonardo de Moura
|
1a4068878e
|
fix(tests/lean/run): adjust tests
|
2015-11-20 16:46:10 -08:00 |
|
Leonardo de Moura
|
5a98a2538c
|
refactor(library): move basic simp/congr rules to init folder, delete some legacy files
|
2015-11-20 16:38:10 -08:00 |
|
Leonardo de Moura
|
eb3d73873a
|
test(tests/lean/run/blast_cc4): congruence_closure and type classes
|
2015-11-20 14:01:15 -08:00 |
|
Leonardo de Moura
|
2627eade8b
|
test(tests/lean/run/blast_cc3): add test for congruence_closure with dependent types
|
2015-11-20 13:55:22 -08:00 |
|
Leonardo de Moura
|
8f368cebbf
|
feat(library/blast/congruence_closure): lift equalities
|
2015-11-20 13:48:22 -08:00 |
|
Leonardo de Moura
|
28970ef717
|
feat(library/blast/congruence_closure): proof extraction
|
2015-11-20 12:23:32 -08:00 |
|
Leonardo de Moura
|
1e3f549c39
|
feat(library/blast/subst_action): add option for disabling subst action
|
2015-11-20 10:53:02 -08:00 |
|
Leonardo de Moura
|
028a2ab785
|
feat(library/blast): add get_config()
|
2015-11-20 10:39:26 -08:00 |
|
Leonardo de Moura
|
c76b04719c
|
feat(library/app_builder): add lift_from_eq
|
2015-11-20 10:27:58 -08:00 |
|
Leonardo de Moura
|
f6ba746b03
|
chore(library/blast/trace): fix signature
|
2015-11-20 08:55:44 -08:00 |
|
Leonardo de Moura
|
ffacf70230
|
chore(library/io_state_stream): remove unused variable
|
2015-11-20 08:20:29 -08:00 |
|
Leonardo de Moura
|
628608ca7d
|
chore(library/blast/congruence_closure): fix style
|
2015-11-19 19:49:59 -08:00 |
|
Leonardo de Moura
|
d5b0a45aa4
|
chore(library/blast/simplifier/simplifier_actions): fix warnings
|
2015-11-19 19:47:04 -08:00 |
|
Daniel Selsam
|
21cb409e6c
|
refactor(library/blast/simplifier): move simplifier module into blast
|
2015-11-19 19:43:04 -08:00 |
|
Daniel Selsam
|
2c72f46adc
|
feat(library/blast/forward): opportunistically delete dead hypotheses
|
2015-11-19 19:40:40 -08:00 |
|
Leonardo de Moura
|
2d93fe4b76
|
feat(library/blast/congruence_closure): implement congruence closure
Proof extraction is still missing
|
2015-11-19 19:37:11 -08:00 |
|
Leonardo de Moura
|
968b615390
|
feat(library/blast/congruence_closure): add "add_eqv"
|
2015-11-19 15:56:21 -08:00 |
|
Leonardo de Moura
|
f9ced4b3e1
|
feat(library/blast): add "ppb" helper class for pretty printing expression in blast
|
2015-11-19 15:55:22 -08:00 |
|
Leonardo de Moura
|
86ad8c348e
|
fix(library/norm_num): memory leaks
|
2015-11-19 14:32:47 -08:00 |
|
Leonardo de Moura
|
ee3083c12c
|
feat(library/blast): add action based on congruence closure module
|
2015-11-19 12:30:45 -08:00 |
|
Leonardo de Moura
|
6bd92e144a
|
test(tests/lean/run/blast20): uncomment example that can now be solved
|
2015-11-19 11:46:22 -08:00 |
|
Leonardo de Moura
|
b1777855cf
|
chore(util/rb_multi_map): remove unnecessary includes
|
2015-11-19 11:45:20 -08:00 |
|
Daniel Selsam
|
5ada4312d7
|
feat(library/blast/forward): propositional forward chaining
|
2015-11-19 11:44:53 -08:00 |
|
Daniel Selsam
|
3523e32345
|
chore(library/blast/simplifier): use blast's app_builder
|
2015-11-19 10:57:33 -08:00 |
|
Daniel Selsam
|
e856de5ab4
|
chore(library/blast/simplifier): remove old comment
|
2015-11-19 10:57:33 -08:00 |
|
Leonardo de Moura
|
193c446fc4
|
fix(library/blast/blast): metavariable assignment validation
|
2015-11-19 10:52:18 -08:00 |
|
Soonho Kong
|
b4b365239f
|
feat(emacs/lean-mode.el): use --dir option in lean-exec-at-pos
See #821 and #788
|
2015-11-19 12:56:07 -05:00 |
|
Leonardo de Moura
|
f78e57fd52
|
feat(shell,frontends/lean): add command line option --dir
See #821
See #788
|
2015-11-19 08:34:23 -08:00 |
|
Leonardo de Moura
|
4bb58a04db
|
fix(CMakeLists): remove tests for dead module, fixes #883
|
2015-11-19 07:59:57 -08:00 |
|
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 |
|
Leonardo de Moura
|
aa1451888c
|
fix(library/blast): spurious trace messages, typo
|
2015-11-18 19:12:29 -08:00 |
|
Leonardo de Moura
|
d85e26898e
|
fix(library/blast): uninitialized variables
|
2015-11-18 18:56:19 -08:00 |
|
Leonardo de Moura
|
fbeee674b3
|
chore(library/blast/union_find): remove dead code
|
2015-11-18 18:35:00 -08:00 |
|
Leonardo de Moura
|
f8a20341cb
|
refactor(library/blast): get_hypothesis_decl return a reference
|
2015-11-18 18:20:02 -08:00 |
|
Leonardo de Moura
|
b61eb3ea0c
|
fix(library/blast): compilation errors in debug mode
|
2015-11-18 18:01:58 -08:00 |
|
Leonardo de Moura
|
808e6f0089
|
chore(library/blast/backward/backward_rule_set): unused variable
|
2015-11-18 17:59:31 -08:00 |
|
Daniel Selsam
|
413989afd6
|
feat(library/blast/backward): backward chaining strategy
|
2015-11-18 17:48:39 -08:00 |
|