michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Commit graph

  • 6f6672eaaa fix(library/blast/discr_tree): ignore annotations in discrimination trees Leonardo de Moura 2016-01-26 18:20:05 -0800
  • 3409deecdb chore(hott): update md files, move port.md Floris van Doorn 2016-01-21 15:31:41 -0500
  • 8eab58f41a fix(choice): make some style changes Floris van Doorn 2016-01-21 15:24:23 -0500
  • 92d6806073 refactor(hott/choice): rename 3.8.5 seulbaek 2016-01-19 16:18:54 -0800
  • 107550238b refactor(hott/choice): rename lemmas for 3.8.2 seulbaek 2016-01-19 16:02:17 -0800
  • d42f3d313f feat(hott): add choice.hlean seulbaek 2016-01-19 15:21:02 -0800
  • 2c81c93d69 feat(hott/types/equiv): add is_trunc_equiv to equiv.hlean seulbaek 2016-01-19 13:20:18 -0800
  • aa5e188179 feat(hott): add symmetry of pushouts and pointed pushouts Jakob von Raumer 2016-01-22 17:06:41 +0000
  • d8d3b0c0b2 feat(hott): add wedge sum of pointed types, neutrality of wedging with the unit type Jakob von Raumer 2016-01-22 14:53:34 +0000
  • 664132b845 feat(hott): add calc lemmas for pointed equivalences, make pinl and pinr constructors Jakob von Raumer 2016-01-22 14:20:30 +0000
  • 8d22e454e7 feat(hott): add theory about pointed pushouts Jakob von Raumer 2016-01-19 21:16:40 +0000
  • b4d8b1db33 fix(library/library.md): update and correct information. Fixes #973. Jeremy Avigad 2016-01-24 17:12:24 -0500
  • 27865e1c8b feat(library/algebra/order_bigops): add min and max over finsets and finite sets Jeremy Avigad 2016-01-24 16:46:31 -0500
  • 53b2d90c90 feat(library/data/{set,finset}): add some useful facts Jeremy Avigad 2016-01-24 16:41:38 -0500
  • 69d953126a refactor(library/algebra/ordered_group,ordered_ring): add versions of classes with decidable linear order, for min and max Jeremy Avigad 2016-01-24 16:35:01 -0500
  • 1980baf784 feat(library/algebra/group_bigops): add Prod_semigroup, for cases without a unit Jeremy Avigad 2016-01-21 17:40:40 -0500
  • 568b3bbeeb feat(library/blast/forward/ematch): trace match-ss Daniel Selsam 2016-01-23 14:50:47 -0800
  • 98fb43e991 fix(library/blast/forward/ematch): advance iterator before continuing Daniel Selsam 2016-01-21 14:44:45 -0800
  • 753d5d0689 fix(library/blast/grind/intro_elim_lemmas): need to copy expr Daniel Selsam 2016-01-21 17:09:34 -0800
  • d12067193b fix(library/blast/forward/pattern): residue computation in the ematching module Leonardo de Moura 2016-01-24 16:15:33 -0800
  • 38ab1cae9e feat(library/blast/unit/unit_propagate): basic support for "dependent lemmas" at unit propagate Leonardo de Moura 2016-01-24 16:02:08 -0800
  • 297ef10611 fix(library/blast/congruence_closure): subsingleton propagation in the congruence closure module Leonardo de Moura 2016-01-24 14:28:43 -0800
  • 3d0ea4c9d1 feat(library/type_context): improve find_unsynth_metavar Leonardo de Moura 2016-01-24 13:39:25 -0800
  • dc5ca99afa fix(library/data/real/basic): unnecessary level of indirection Leonardo de Moura 2016-01-24 13:37:15 -0800
  • b2554dcb8f fix(library/blast/congruence_closure): cannot assume all subterms have been internalized Daniel Selsam 2016-01-16 11:54:06 -0800
  • 19bfbe2df8 fix(library/blast/congruence_closure): uselist initialization (aka add_occurrence) Leonardo de Moura 2016-01-16 19:53:36 -0800
  • 1d04160a9b fix(library/blast/congruence_closure): bug at eq_congr_key_cmp::operator()(eq_congr_key const & k1, eq_congr_key const & k2) Leonardo de Moura 2016-01-16 19:33:24 -0800
  • 7e11c5cf6e fix(src/util/file_lock): ignore failure to create locks on read-only file systems Gabriel Ebner 2016-01-16 09:26:45 +0100
  • 86fc326e08 refactor/feat(library/theories/analysis/*): reorganize analysis library and add some theorems Jeremy Avigad 2016-01-14 23:57:27 -0500
  • 98319139d9 fix(library/blast/forward/ematch): bug in match_leaf Leonardo de Moura 2016-01-16 10:51:00 -0800
  • a883101a3b feat(library/blast/forward/ematch): basic support for heq classes Daniel Selsam 2016-01-15 20:34:28 -0800
  • f2eef7aa1b feat(emacs): use s-join instead of string-join Syohei YOSHIDA 2016-01-14 20:35:59 +0900
  • 885c62648f fix(emacs/lean-option.el): don't use deprecated function, string-to-int Syohei YOSHIDA 2016-01-14 12:50:54 +0900
  • 60861d7dea chore(tests/lean/run/blast_cc_heq9): make sure that only congruence closure module is used Leonardo de Moura 2016-01-13 22:13:04 -0800
  • 37fdac4d65 test(tests/lean/run/blast_cc_heq9): add new test Leonardo de Moura 2016-01-13 22:10:15 -0800
  • abbffc7436 feat(library/blast/forward/ematch): more tracing Daniel Selsam 2016-01-13 19:16:54 -0800
  • 7a005fb76b test(tests/lean/run/blast_vector_test): more tests Daniel Selsam 2016-01-13 21:05:22 -0800
  • 8d49e42ec2 fix(library/blast/congruence_closure): user-defined congruence lemmas for equality and relation congruences Leonardo de Moura 2016-01-13 21:59:12 -0800
  • 3f7122ce07 feat(library/blast/congruence_closure): more general congruence lemmas Leonardo de Moura 2016-01-13 21:44:32 -0800
  • d9294fc164 chore(kernel/expr): remove dead var Leonardo de Moura 2016-01-13 17:36:33 -0800
  • f0cc98ebb5 chore(library/blast/recursor/recursor_action): disable spurious warning Leonardo de Moura 2016-01-13 17:28:13 -0800
  • 1048812e2e chore(frontends/lean/notation_cmd): cleanup weird coding pattern Leonardo de Moura 2016-01-13 17:27:25 -0800
  • 912c5254de fix(tests/lean/run/cases_bug): adjust test to changes in the std lib Leonardo de Moura 2016-01-13 16:37:33 -0800
  • 05c3ede683 feat(tests/lean/run/blast_vector_test): test ematch + cc at vectors Leonardo de Moura 2016-01-13 16:33:45 -0800
  • b1d32bbaf6 chore(library/blast/forward/ematch): more tracing Leonardo de Moura 2016-01-13 16:28:09 -0800
  • ba16d188e6 feat(library/blast/forward/ematch): basic debug tracing Daniel Selsam 2016-01-13 11:28:49 -0800
  • 58d41e486c feat(library/trace): register debug trace class Daniel Selsam 2016-01-13 11:28:28 -0800
  • 599ec08c70 feat(library/blast/congruence_closure): add support for eq.rec and cast in the congruence closure module Leonardo de Moura 2016-01-13 14:18:38 -0800
  • b975717875 feat(init/logic): add cast_heq Leonardo de Moura 2016-01-13 14:18:01 -0800
  • c19be9d9e7 feat(library/util): add is_app_of helper function Leonardo de Moura 2016-01-13 13:33:30 -0800
  • 723a9e227a chore(kernel/default_converter): remove dead code Leonardo de Moura 2016-01-13 13:33:13 -0800
  • 8fded5224b chore(library/blast/congruence_closure): improve comment Leonardo de Moura 2016-01-13 13:06:09 -0800
  • 3643e79cb3 feat(library/blast/congruence_closure): improve the suppoer for subsingletons in the ematching procedure Leonardo de Moura 2016-01-13 11:01:59 -0800
  • 8f7b533ca1 refactor(library): move 'cast' to init folder Leonardo de Moura 2016-01-13 10:55:54 -0800
  • f7494618ff fit(emacs/lean-input.el): fix loading cl.el at runtime Syohei YOSHIDA 2016-01-13 17:59:33 +0900
  • 5903fe4287 feat(emacs): use cl-lib functions/macros instead of cl.el Syohei YOSHIDA 2016-01-13 17:59:02 +0900
  • 081ad1212b test(tests/lean/run/blast_ematch_list): blast last_concat Leonardo de Moura 2016-01-12 22:56:28 -0800
  • 12876ccc20 fix(library/blast/forward/ematch): ematch + subsingleton Leonardo de Moura 2016-01-12 22:31:09 -0800
  • c2b6e3c29c fix(library/blast/recursor/recursor_strategy): deactivate hypotheses before invoking nested strategy Leonardo de Moura 2016-01-12 18:41:14 -0800
  • 292f28e769 test(tests/lean/run/blast_tuple): more tests for blast + tuple Daniel Selsam 2016-01-11 16:53:31 -0800
  • d736376a6f test(tests/lean/run/blast_cc_heq8): new congruence closure procedure can also handle subtypes without using a flattening preprocessing step Leonardo de Moura 2016-01-11 16:50:03 -0800
  • b40f0ffe8b fix(library/blast/forward/ematch): keep using ematching on implicit arguments Leonardo de Moura 2016-01-11 15:40:51 -0800
  • 1c5418ac2e test(tests/lean/run): add example/test for blast + tuples Leonardo de Moura 2016-01-11 12:17:14 -0800
  • bb759b1a90 feat(library/blast/congruence_closure): use blast.cc.heq by default Leonardo de Moura 2016-01-11 11:59:54 -0800
  • 5edcccaeb0 feat(library/blast/forward/ematch): add support for the new hcongr lemmas in the ematching module Leonardo de Moura 2016-01-11 11:10:47 -0800
  • 32268b71d2 feat(library/app_builder): avoid redundant heq_of_eq(eq_of_heq(H)) proofs Leonardo de Moura 2016-01-10 19:29:34 -0800
  • ddff37dd0f fix(library/blast/congruence_closure): bug when using blast.cc.heq and handling relation congruences Leonardo de Moura 2016-01-10 19:28:55 -0800
  • 2b38d0fe9b chore(library/app_builder): improve trace message Leonardo de Moura 2016-01-10 18:31:38 -0800
  • f22ba4e641 feat(library/type_context): cache mk_subsingleton_instance Leonardo de Moura 2016-01-10 18:26:40 -0800
  • 799317c43e fix(library/blast/congruence_closure): add missing eq => heq lifting Leonardo de Moura 2016-01-10 18:03:35 -0800
  • cf8307ee20 feat(library/app_builder): use types in app_builder trace messages Leonardo de Moura 2016-01-10 17:29:11 -0800
  • 3a846a28a3 feat(library/blast/congruence_closure): support for subsingleton propagation Leonardo de Moura 2016-01-10 17:24:12 -0800
  • c646c3cacc feat(library/init/logic): add subsingleton.helim with heterogeneous equality Leonardo de Moura 2016-01-10 16:47:45 -0800
  • 6c015a4954 feat(library/blast/blast): use blast tmp_type_context to generate type class instances Leonardo de Moura 2016-01-10 16:30:51 -0800
  • 912bccb3f9 fix(library/blast/congruence_closure): do not adjust proofs when blast.cc.heq == false Leonardo de Moura 2016-01-10 15:28:16 -0800
  • e9d24ec152 feat(library/blast/congruence_closure): create simpler congruence proofs when using blast.cc.heq Leonardo de Moura 2016-01-10 15:11:31 -0800
  • ea7da31bba feat(library/blast/congruence_closure): support for congruence lemmas that use heterogeneous equality Leonardo de Moura 2016-01-10 13:45:40 -0800
  • 934f3b67ff feat(library/blast/congruence_closure): basic support for heterogeneous equality Leonardo de Moura 2016-01-10 12:41:30 -0800
  • 22a6b7f1c3 feat(library/blast/congruence_closure): add blast.cc.heq option Leonardo de Moura 2016-01-10 00:15:26 -0800
  • b7be3ec6de test(tests/lean/run): add tests for heterogeneous congruence lemma generator Leonardo de Moura 2016-01-09 16:18:39 -0800
  • 437b0fb4ee feat(library/congr_lemma_manager): cache hcongr lemmas Leonardo de Moura 2016-01-09 15:48:17 -0800
  • 42cdda227a feat(library/congr_lemma_manager): add heterogeneous equality congruence lemmas Leonardo de Moura 2016-01-09 15:41:08 -0800
  • 403966792d feat(library/app_builder): add helper heq methods Leonardo de Moura 2016-01-09 12:46:14 -0800
  • d3242a2068 refactor(library): rename heq.of_eq heq.to_eq auxiliary lemmas Leonardo de Moura 2016-01-09 12:32:18 -0800
  • af42d3ff2d fix(emacs/load-lean.el): add seq to lean-required-packages Soonho Kong 2016-01-08 03:35:23 +0000
  • 27eea05da9 fix(library/blast/discr_tree): bug in the discrimination tree module Leonardo de Moura 2016-01-06 17:30:44 -0800
  • 3c22a9d4e1 feat(library/blast/recursor/recursor_strategy): add new options to control recursor/recursion strategy Leonardo de Moura 2016-01-06 17:30:38 -0800
  • 4e8ae94aba chore(tests/lean/run/blast_cc_noconfusion): make sure simp/subst are not used in the test Leonardo de Moura 2016-01-06 17:30:31 -0800
  • 76cebb45f9 feat(library/blast/congruence_closure): add support for 'no_confusion' in the congruence closure module Leonardo de Moura 2016-01-06 17:30:25 -0800
  • cb02d1deae feat(library/blast/congruence_closure): add support for specialized congr lemmas in the congruence closure module Leonardo de Moura 2016-01-06 17:30:20 -0800
  • ef691d6cf5 fix(library/abstract_expr_manager): bug introduced today Leonardo de Moura 2016-01-06 17:30:14 -0800
  • c9930d0a29 feat(library/blast/simplifier/simplifier): subsingleton normalization for application arguments and lambdas Leonardo de Moura 2016-01-06 17:30:08 -0800
  • e7bcb89314 fix(library/simplifier/simplifier): bug in cache_lookup Leonardo de Moura 2016-01-06 17:30:01 -0800
  • 14d4ae7e97 chore(library/blast/simplifier/simplifier): remove dead variable Leonardo de Moura 2016-01-06 17:29:54 -0800
  • 9fa1a7a01c refactor(abstract_expr_manager): use get_specialization_prefix_size to improve performance of abstract_expr_manager Leonardo de Moura 2016-01-06 17:29:48 -0800
  • d4a5aa6db0 refactor(library/fun_info_manager): improve performance and add get_prefix method Leonardo de Moura 2016-01-06 17:29:41 -0800
  • f3b8aef24c feat(library/fun_info_manager,library/congr_lemma_manager,blast/simplifier): specialized congruence lemmas Leonardo de Moura 2016-01-06 17:29:35 -0800
  • 930fcddace feat(kernel/expr): add get_app_args_at_most Leonardo de Moura 2016-01-06 17:29:28 -0800
  • 9a1a9f3b5a refactor(library/fun_info_manager): use expr_unsigned_map Leonardo de Moura 2016-01-06 17:29:22 -0800
  • 7312dd77b8 refactor(library/congr_lemma_manager): move expr_unsigned_map to separate module Leonardo de Moura 2016-01-06 17:29:16 -0800