michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
8342 commits 3 branches 0 tags 28 MiB
Commit graph

8342 commits

This branch
This branch
All branches
Author SHA1 Message Date
Syohei YOSHIDA
f2eef7aa1b feat(emacs): use s-join instead of string-join 
Because string-join was introduced at Emacs 24.4 and subr-x.el must be
loaded for using it.
 2016-01-14 09:36:52 -05:00
Syohei YOSHIDA
885c62648f fix(emacs/lean-option.el): don't use deprecated function, string-to-int 
string-to-int was deprecated since Emacs 22.
string-to-number should be used instead of string-to-int.
 2016-01-14 09:36:37 -05:00
Leonardo de Moura
60861d7dea chore(tests/lean/run/blast_cc_heq9): make sure that only congruence closure module is used 2016-01-13 22:13:04 -08:00
Leonardo de Moura
37fdac4d65 test(tests/lean/run/blast_cc_heq9): add new test 2016-01-13 22:10:15 -08:00
Daniel Selsam
abbffc7436 feat(library/blast/forward/ematch): more tracing 2016-01-13 22:04:12 -08:00
Daniel Selsam
7a005fb76b test(tests/lean/run/blast_vector_test): more tests 2016-01-13 22:03:47 -08:00
Leonardo de Moura
8d49e42ec2 fix(library/blast/congruence_closure): user-defined congruence lemmas for equality and relation congruences 2016-01-13 21:59:38 -08:00
Leonardo de Moura
3f7122ce07 feat(library/blast/congruence_closure): more general congruence lemmas 2016-01-13 21:44:32 -08:00
Leonardo de Moura
d9294fc164 chore(kernel/expr): remove dead var 2016-01-13 17:36:33 -08:00
Leonardo de Moura
f0cc98ebb5 chore(library/blast/recursor/recursor_action): disable spurious warning 2016-01-13 17:28:13 -08:00
Leonardo de Moura
1048812e2e chore(frontends/lean/notation_cmd): cleanup weird coding pattern 2016-01-13 17:27:25 -08:00
Leonardo de Moura
912c5254de fix(tests/lean/run/cases_bug): adjust test to changes in the std lib 2016-01-13 16:37:33 -08:00
Leonardo de Moura
05c3ede683 feat(tests/lean/run/blast_vector_test): test ematch + cc at vectors 2016-01-13 16:35:21 -08:00
Leonardo de Moura
b1d32bbaf6 chore(library/blast/forward/ematch): more tracing 2016-01-13 16:28:09 -08:00
Daniel Selsam
ba16d188e6 feat(library/blast/forward/ematch): basic debug tracing 2016-01-13 15:15:15 -08:00
Daniel Selsam
58d41e486c feat(library/trace): register debug trace class 2016-01-13 15:15:15 -08:00
Leonardo de Moura
599ec08c70 feat(library/blast/congruence_closure): add support for eq.rec and cast in the congruence closure module 2016-01-13 14:18:38 -08:00
Leonardo de Moura
b975717875 feat(init/logic): add cast_heq 2016-01-13 14:18:01 -08:00
Leonardo de Moura
c19be9d9e7 feat(library/util): add is_app_of helper function 2016-01-13 13:33:30 -08:00
Leonardo de Moura
723a9e227a chore(kernel/default_converter): remove dead code 2016-01-13 13:33:13 -08:00
Leonardo de Moura
8fded5224b chore(library/blast/congruence_closure): improve comment 2016-01-13 13:06:09 -08:00
Leonardo de Moura
3643e79cb3 feat(library/blast/congruence_closure): improve the suppoer for subsingletons in the ematching procedure 2016-01-13 11:17:42 -08:00
Leonardo de Moura
8f7b533ca1 refactor(library): move 'cast' to init folder 2016-01-13 11:17:42 -08:00
Syohei YOSHIDA
f7494618ff fit(emacs/lean-input.el): fix loading cl.el at runtime 
This package uses only cl.el macro(lexical-let). So it is enough to
load cl.el at compile time.
 2016-01-13 11:19:53 -05:00
Syohei YOSHIDA
5903fe4287 feat(emacs): use cl-lib functions/macros instead of cl.el 2016-01-13 11:19:40 -05:00
Leonardo de Moura
081ad1212b test(tests/lean/run/blast_ematch_list): blast last_concat 2016-01-12 22:56:28 -08:00
Leonardo de Moura
12876ccc20 fix(library/blast/forward/ematch): ematch + subsingleton 2016-01-12 22:31:09 -08:00
Leonardo de Moura
c2b6e3c29c fix(library/blast/recursor/recursor_strategy): deactivate hypotheses before invoking nested strategy 2016-01-12 18:41:14 -08:00
Daniel Selsam
292f28e769 test(tests/lean/run/blast_tuple): more tests for blast + tuple 2016-01-11 17:37:44 -08:00
Leonardo de Moura
d736376a6f test(tests/lean/run/blast_cc_heq8): new congruence closure procedure can also handle subtypes without using a flattening preprocessing step 2016-01-11 16:50:03 -08:00
Leonardo de Moura
b40f0ffe8b fix(library/blast/forward/ematch): keep using ematching on implicit arguments 
Ematching module should only ignore type classes (i.e., instance
implicit) and subsingletons (which includes propositions).
 2016-01-11 15:40:51 -08:00
Leonardo de Moura
1c5418ac2e test(tests/lean/run): add example/test for blast + tuples 2016-01-11 12:17:14 -08:00
Leonardo de Moura
bb759b1a90 feat(library/blast/congruence_closure): use blast.cc.heq by default 2016-01-11 11:59:54 -08:00
Leonardo de Moura
5edcccaeb0 feat(library/blast/forward/ematch): add support for the new hcongr lemmas in the ematching module 2016-01-11 11:56:36 -08:00
Leonardo de Moura
32268b71d2 feat(library/app_builder): avoid redundant heq_of_eq(eq_of_heq(H)) proofs 2016-01-10 19:29:34 -08:00
Leonardo de Moura
ddff37dd0f fix(library/blast/congruence_closure): bug when using blast.cc.heq and handling relation congruences 2016-01-10 19:28:55 -08:00
Leonardo de Moura
2b38d0fe9b chore(library/app_builder): improve trace message 2016-01-10 18:31:54 -08:00
Leonardo de Moura
f22ba4e641 feat(library/type_context): cache mk_subsingleton_instance 2016-01-10 18:26:40 -08:00
Leonardo de Moura
799317c43e fix(library/blast/congruence_closure): add missing eq => heq lifting 2016-01-10 18:03:35 -08:00
Leonardo de Moura
cf8307ee20 feat(library/app_builder): use types in app_builder trace messages 2016-01-10 17:29:11 -08:00
Leonardo de Moura
3a846a28a3 feat(library/blast/congruence_closure): support for subsingleton propagation 2016-01-10 17:24:12 -08:00
Leonardo de Moura
c646c3cacc feat(library/init/logic): add subsingleton.helim with heterogeneous equality 2016-01-10 16:47:45 -08:00
Leonardo de Moura
6c015a4954 feat(library/blast/blast): use blast tmp_type_context to generate type class instances 2016-01-10 16:30:51 -08:00
Leonardo de Moura
912bccb3f9 fix(library/blast/congruence_closure): do not adjust proofs when blast.cc.heq == false 2016-01-10 15:28:16 -08:00
Leonardo de Moura
e9d24ec152 feat(library/blast/congruence_closure): create simpler congruence proofs when using blast.cc.heq 2016-01-10 15:11:31 -08:00
Leonardo de Moura
ea7da31bba feat(library/blast/congruence_closure): support for congruence lemmas that use heterogeneous equality 2016-01-10 13:45:40 -08:00
Leonardo de Moura
934f3b67ff feat(library/blast/congruence_closure): basic support for heterogeneous equality 
We still have to process the general congruence lemmas.
 2016-01-10 12:53:05 -08:00
Leonardo de Moura
22a6b7f1c3 feat(library/blast/congruence_closure): add blast.cc.heq option 2016-01-10 00:15:52 -08:00
Leonardo de Moura
b7be3ec6de test(tests/lean/run): add tests for heterogeneous congruence lemma generator 2016-01-09 16:18:39 -08:00
Leonardo de Moura
437b0fb4ee feat(library/congr_lemma_manager): cache hcongr lemmas 2016-01-09 15:48:17 -08:00