lean2

michael/lean2

Fork 0

Commit graph

43c5cbd1bf feat(library/fun_info_manager): more general fun_info_manager Leonardo de Moura 2016-01-06 17:29:10 -0800
3ca785b0e7 refactor(library/fun_info_manager): remove dead code Leonardo de Moura 2016-01-06 17:29:02 -0800
a992bb46a6 feat(library/fun_info_manager): update interface Leonardo de Moura 2016-01-06 17:28:52 -0800
12571c92d8 refactor(library/algebra): explicit parameters also for fun instances Johannes Hölzl 2016-01-06 16:20:38 +0100
6d6a00f48b refactor(library/algebra): fix theorem names Johannes Hölzl 2016-01-06 16:13:39 +0100
f7ea9a5f64 feat(library/algebra): add theory about Galois connections Johannes Hölzl 2016-01-04 22:15:02 +0100
9c28552afb feat(library/algebra): add lattice instances for Prop, fun, and set Johannes Hölzl 2016-01-04 22:03:47 +0100
c0deac6a63 fix(src/emacs): add replace keyword to emacs syntax file Rob Lewis 2016-01-05 11:01:00 -0500
a57b7fadfb style(replace_tactic): remove extra whitespace Rob Lewis 2016-01-04 15:10:51 -0500
458725e63f feat(library/algebra): add missing theorems to group and ordered ring Rob Lewis 2016-01-04 14:45:39 -0500
031831f101 feat(library/tactic): add replace tactic Rob Lewis 2016-01-04 14:43:31 -0500
ba392f504f feat(kernel/expr,library/blast/blast,frontends/lean/decl_cmds): add workaround for allowing users to use blast inside of recursive equations Leonardo de Moura 2016-01-03 21:51:21 -0800
a22346e411 fix(lean/tests/lean/run/new_obtain{3,4}): adapt tests to new notation for image Jeremy Avigad 2016-01-03 21:40:56 -0500
d9118ded76 feat(library/theories/topology/basic): show that generated topology is initial Jeremy Avigad 2016-01-03 21:25:09 -0500
4289daddcb refactor(library/data/{set,finset}/basic,library/*): change notation for image to tick mark Jeremy Avigad 2016-01-03 19:41:01 -0500
17f6ab3a71 fix(library/data/set/basic): fix spacing in notation Jeremy Avigad 2016-01-03 18:24:18 -0500
7600d04533 library/algebra/complete_lattice): fix typo in comment Jeremy Avigad 2016-01-03 18:21:26 -0500
173368801b fix(library/algebra/interval): rename namespace, and move a theorem Jeremy Avigad 2016-01-03 18:19:45 -0500
31aa256b99 feat(library/theories/measure_theory/sigma_algebra): start with definition and properties of sigma algebras Jeremy Avigad 2016-01-03 18:11:10 -0500
721f6c87bf feat(library/data/set/basic): add some theorems Jeremy Avigad 2016-01-03 18:03:15 -0500
4478d570bd chore(library/congr_lemma_manager): fix style Leonardo de Moura 2016-01-03 18:02:50 -0800
19ebedd480 feat(library/type_context): improve type_context get_level_core, add virtual method for checking types whenever a metavariable is assigned Leonardo de Moura 2016-01-03 17:58:27 -0800
1fc7bbceb2 chore(frontends/lean/builtin_cmds): handle FixedNoParam in the front-end Leonardo de Moura 2016-01-03 15:18:26 -0800
fcf532ea67 chore(library/app_builder): fix typo in trace message Leonardo de Moura 2016-01-03 15:16:50 -0800
d0fe59ef8a feat(library/congr_lemma_manager): add new kind of congr_arg Leonardo de Moura 2016-01-03 15:10:07 -0800
67d49aabd9 chore(library/congr_lemma_manager): document main methods Leonardo de Moura 2016-01-03 14:39:19 -0800
66a722ff5a feat(library/unifier): remove "eager delta hack", use is_def_eq when delta-constraint does not have metavariables anymore Leonardo de Moura 2016-01-03 12:39:32 -0800
d02ead320a feat(library/unifier): remove unifier.computation option Leonardo de Moura 2016-01-03 11:00:16 -0800
9935cbc3d7 feat(library/blast/blast): communicate assigned metavariables back to tactic framework Leonardo de Moura 2016-01-02 20:05:44 -0800
56d9b6b0d3 fix(library/blast/blast): convert uref and mref back into tactic metavariables Leonardo de Moura 2016-01-02 19:22:40 -0800
d85b4300b1 fix(library/blast/blast): bug at visit_meta_app Leonardo de Moura 2016-01-02 19:08:56 -0800
5feef27c2b feat(frontends/lean/notation_cmd): relax restriction on user defined tokens Leonardo de Moura 2016-01-02 13:58:46 -0800
4eb2690c32 feat(library/scoped_ext): store set of opened namespaces Leonardo de Moura 2016-01-02 13:35:08 -0800
155df48665 feat(library): remove decl_stats Leonardo de Moura 2016-01-02 12:59:42 -0800
befe41e8f5 fix(tests/lean): adjust tests Leonardo de Moura 2016-01-02 12:51:20 -0800
3c564fcc55 fix(library/user_recursors): 'print recursor-lemma' command Leonardo de Moura 2016-01-01 18:12:12 -0800
0963ce336f feat(library/blast): add 'grind' and 'grind_simp' blast strategies Leonardo de Moura 2016-01-01 17:32:13 -0800
57c9ced111 feat(library/blast): add fail_action and fail_strategy helper functions Leonardo de Moura 2016-01-01 17:18:05 -0800
cd7708d556 feat(library/blast/backward/backward_strategy): add extensible backward chaining strategy Leonardo de Moura 2016-01-01 17:07:15 -0800
43f0183ce9 feat(library/blast/backward/backward_strategy): allow user to control the number of nested backward chaining steps Leonardo de Moura 2016-01-01 16:46:49 -0800
17a2f1fe47 chore(tests/lean/run/blast_grind1): use 'core_grind' Leonardo de Moura 2016-01-01 16:46:15 -0800
4f1415174e refactor(library/data): "union." ==> "union_", "inter." ==> "inter_" Leonardo de Moura 2016-01-01 16:13:44 -0800
4e2494f12e refactor(library/init/nat): minor cleanup Leonardo de Moura 2016-01-01 15:56:46 -0800
ac9d6c2021 refactor(library/data/bool): cleanup bool proofs and fix bxor definition Leonardo de Moura 2016-01-01 13:52:42 -0800
52ec7e6d57 feat(library/blast/recursor): add 'blast.recursor.max_rounds' options and iterative deepening for recursor_strategy Leonardo de Moura 2016-01-01 13:09:37 -0800
1bb21d202b refactor(library/blast): move recursor action and strategy to its own directory Leonardo de Moura 2016-01-01 12:45:31 -0800
317c32a7e2 fix(library/blast/state): avoid duplicated names at state::to_goal Leonardo de Moura 2016-01-01 00:10:54 -0800
712e19e22a fix(library/blast/forward/ematch): bug in the ematching procedure Leonardo de Moura 2015-12-31 21:26:44 -0800
54f2c0f254 feat(library/blast/forward): inst_simp should use the left-hand-side as a pattern (if none is provided by the user) Leonardo de Moura 2015-12-31 20:20:39 -0800
03f9e9acb0 feat(library/blast/forward): display lemma name when printing instance Leonardo de Moura 2015-12-31 18:09:17 -0800
9dd1302dac chore(extras/latex/lstlean.tex): update list of modifiers Jeremy Avigad 2015-12-31 17:12:37 -0500
0fb398c217 fix(library/data/nat/bigops): delete some blank lines Jeremy Avigad 2015-12-31 13:23:52 -0800
e14a2aaf3c feat(doc/lean/library_style.org): clarify C_of_A_of_B convention Jeremy Avigad 2015-12-31 12:59:31 -0800
7f25dd6646 feat(library/data/nat/bigops): sums and products over intervals of natural numbers Jeremy Avigad 2015-12-31 12:51:20 -0800
12a69bad04 refactor(library/data/finset/basic,library/*): get rid of finset singleton Jeremy Avigad 2015-12-31 11:50:55 -0800
8a00a431e8 refactor(library/data/finset/basic): rename theorem Jeremy Avigad 2015-12-31 10:50:11 -0800
a28ded641c refactor(library/algebra/interval): rename intervals to interval Jeremy Avigad 2015-12-31 10:48:39 -0800
86b64cf43b feat(library/data/set/*,library/algebra/group_bigops): better finiteness lemmas, reindexing for big operations Jeremy Avigad 2015-12-31 10:42:51 -0800
c3dfabf741 feat(library/blast/strategies/portfolio): add 'rec_simp' Leonardo de Moura 2015-12-31 15:00:38 -0800
4134fdd925 feat(library/blast/strategies/rec_strategy): give priority to user defined recursors Leonardo de Moura 2015-12-31 14:54:31 -0800
76677c4535 feat(library/blast/actions/assert_cc_action): add target_cc_action Leonardo de Moura 2015-12-31 14:53:55 -0800
fdcdfbf385 feat(library/blast/simplifier/simplifier_actions): only add symplified hypothesis if it is not "true" Leonardo de Moura 2015-12-31 14:25:38 -0800
bd03619b5c refactor(library/data/list/basic): test 'rec_inst_simp' blast strategy Leonardo de Moura 2015-12-31 13:03:47 -0800
b35abcc6a8 refactor(library): rename strategy "msimp" ==> "inst_simp" Leonardo de Moura 2015-12-31 12:45:48 -0800
4cf5c77575 feat(library/blast/strategies): add strategy for applying recursors Leonardo de Moura 2015-12-31 12:35:16 -0800
20b585c432 feat(library/blast/forward/ematch): use blast.event.ematch for ematch module abnormal behavior Leonardo de Moura 2015-12-31 12:25:50 -0800
935a2536ec fix(library/blast/actions/recursor_action): must normalize target for each subgoal Leonardo de Moura 2015-12-31 12:25:17 -0800
ba2cdc848a feat(library/util, library/pp_options): add pp.goal.max_hypotheses Leonardo de Moura 2015-12-30 12:38:03 -0800
23836f53bb feat(library/blast): do not display inactive hypotheses when displaying failure states Leonardo de Moura 2015-12-30 12:08:33 -0800
f2d4e81889 fix(library/blast/state): inactive hypotheses should be printed "after" active ones Leonardo de Moura 2015-12-30 11:46:41 -0800
2a454ce791 chore(library/blast/state): do not display set of active hypotheses Leonardo de Moura 2015-12-30 11:31:59 -0800
dc6a3e30c0 refactor(library): test simp and msimp in the standard library Leonardo de Moura 2015-12-30 11:22:58 -0800
251b53c669 refactor(library/blast/strategies): rename 'debug_action_strategy' to 'action_strategy' Leonardo de Moura 2015-12-29 20:45:24 -0800
41a01bb606 feat(library/blast/forward/ematch): add option 'blast.ematch.max_instances' Leonardo de Moura 2015-12-29 20:36:11 -0800
0148bb08fd feat(library/blast): add 'ematch_simp' strategy for blast and msimp shortcut for it. Leonardo de Moura 2015-12-29 20:04:31 -0800
8c87f90a29 feat(frontends/lean/elaborator): avoid redudant "don't know how to synthesize placeholder" when using flycheck Leonardo de Moura 2015-12-29 18:00:19 -0800
86a5379a96 feat(library/blast): include strategies failure states in the tactic_exception Leonardo de Moura 2015-12-29 17:08:33 -0800
b92416d66c refactor(library/error_handling): move error_handling to library main dir Leonardo de Moura 2015-12-29 15:31:40 -0800
7462874a4a refactor(library): cleanup nat/int proofs Leonardo de Moura 2015-12-29 12:39:53 -0800
a307a0691b refactor(library/data/nat/basic): cleanup some of the nat proofs Leonardo de Moura 2015-12-29 11:43:56 -0800
726867a8fb refactor(library/algebra/ring): minor cleanup Leonardo de Moura 2015-12-29 11:16:18 -0800
3557bd36e7 refactor(library/algebra/group): cleanup proofs using simp and add [simp] attribute Leonardo de Moura 2015-12-29 10:48:47 -0800
b117a10f82 refactor(library/blast/simplifier): use priority_queue to store simp/congr lemmas, use name convention used at forward/backward lemmas, normalize lemmas when blast starts, cache get_simp_lemmas Leonardo de Moura 2015-12-28 17:52:57 -0800
5b7dc31ad1 chore(library/blast/backward): remove unnecessary include Leonardo de Moura 2015-12-28 14:26:18 -0800
079a25f770 refactor(library/blast/forward): make sure backward and forward modules use same naming convention Leonardo de Moura 2015-12-28 12:37:16 -0800
482ffe4242 fix(library/attribute_manager): memory leak Leonardo de Moura 2015-12-28 12:31:38 -0800
c8b9c98eb6 refactor(library/blast/backward): use priority_queue, make sure head is normalized when building index Leonardo de Moura 2015-12-28 12:10:56 -0800
26d0a62052 refactor(*): make sure we use LEAN_DEFAULT_PRIORITY Leonardo de Moura 2015-12-28 10:47:56 -0800
f177082c3b refactor(*): normalize metaclass names Leonardo de Moura 2015-12-28 10:30:23 -0800
96bec8b4f9 fix(frontends/lean/builtin_cmds): allow token and metaclass to have the same name Leonardo de Moura 2015-12-28 09:57:45 -0800
89a5d00714 chore(library/blast): style Leonardo de Moura 2015-12-28 08:52:24 -0800
f679ce0da9 refactor(frontends/lean): move 'print_cmd' to separate module Leonardo de Moura 2015-12-26 21:13:59 -0500
cac10aa728 fix(frontends/lean/parser): allow '...' token to be used in imports Leonardo de Moura 2015-12-26 19:59:11 -0500
2a5a904416 feat(library/blast/discr_tree): remove hack for setting m_fn flag Leonardo de Moura 2015-12-26 15:27:34 -0500
93b912ec89 feat(library/blast): use discrimination trees instead of head_map for indexing hypotheses Leonardo de Moura 2015-12-26 15:13:27 -0500
1f1fafd535 feat(library/blast/discr_tree): erase operation Leonardo de Moura 2015-12-26 13:41:15 -0500
45c29d422f feat(library/blast/discr_tree): set edge m_fn flag Leonardo de Moura 2015-12-26 13:11:57 -0500
43e1292f22 feat(library/blast): add discrimination trees Leonardo de Moura 2015-12-21 06:20:15 -0800
b09fdc8c61 feat(hott/hit): flattening lemmas for coeq and pushout Ulrik Buchholtz 2015-12-25 15:11:11 -0500
f3b2c7010f feat(hott): functoriality of quotients Ulrik Buchholtz 2015-12-19 18:13:02 -0500