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

Commit graph

  • fe66e2aa4a fix(tests/lean): subtype notation is not in the top-level anymore Leonardo de Moura 2015-12-28 09:04:11 -0800
  • c52ffda0e0 feat(library/algebra/intervals): add notation for intervals Jeremy Avigad 2015-12-26 10:45:53 -0800
  • 395eab7c2c feat(library/theories/topology/basic): start on topology (with Jacob Gross) Jeremy Avigad 2015-12-26 10:29:58 -0800
  • 549feb5d7f feat(library/data/set/basic): add notation and theorems for large unions and intersections Jeremy Avigad 2015-12-26 08:02:04 -0800
  • d83e5d25fc feat(library/theories/measure_theory/extended_real): start on extended reals Jeremy Avigad 2015-12-24 16:27:48 -0500
  • 84cdf3d36d feat(library/theories/analysis/normed_space): start theory of normed spaces for analysis Jeremy Avigad 2015-12-22 16:28:14 -0500
  • 08fbf127c6 feat(library/theories/analysis/metric_space,real_limit): define complete metric space, make real an instance Jeremy Avigad 2015-12-22 13:25:38 -0500
  • 5b3fbf1618 feat(library/algebra/module): make a start on modules and vector spaces (with material from Nathaniel Thomas) Jeremy Avigad 2015-12-22 12:54:42 -0500
  • dc8cad10bf feat(src/emacs/README.md): add header Jeremy Avigad 2015-12-21 16:40:36 -0500
  • 6913eb0c76 refactor(library/init/subtype.lean): put subtype notation in the namespace Jeremy Avigad 2015-12-21 16:19:37 -0500
  • 68ecdc4c26 feat(src/emacs/README.md): expand instructions slightly Jeremy Avigad 2015-12-21 16:17:38 -0500
  • 8d50405e68 chore(library/extras/latex/lstlean.text): update lists for syntax highlighting Jeremy Avigad 2015-12-21 15:54:00 -0500
  • 8ccafc4267 fix(library/init/function): fix typo Jeremy Avigad 2015-12-21 15:44:44 -0500
  • baf11d0018 feat(library/algebra/ring_bigops): make start on file with more properties of sums and products Jeremy Avigad 2015-12-19 15:45:24 -0500
  • 0e3b13f1a0 refactor(library/algebra): combine group_bigops and group_set_bigops Jeremy Avigad 2015-12-19 14:10:20 -0500
  • f1daf8f24e fix(algebra/group.lean): remove unnecessary use of add.assoc from theorem bit0_add_bit1_helper Soonho Kong 2015-12-22 09:12:57 -0500
  • 71cad16c32 fix(extras/depgraph): calculate lean executable path from PATH or guess Ulrik Buchholtz 2015-12-19 22:55:58 -0500
  • f911747b60 fix(util/file_lock.cpp): add 'include <fcntl.h>' Soonho Kong 2015-12-19 07:51:00 -0500
  • 43a8b01211 feat(extra/depgraph): add dependency graph script Soonho Kong 2015-12-18 18:28:58 -0500
  • c5223d2d19 fix(emacs/load-lean.el): proceed even if logo image is not created Soonho Kong 2015-12-18 14:28:54 -0500
  • a7d1625765 fix(library/blast/forward/forward_lemma_set): check pattern inference when setting attribute Leonardo de Moura 2015-12-17 22:50:14 -0800
  • 9a6bd96d6b chore(frontends/lean/decl_attributes): style Leonardo de Moura 2015-12-17 22:50:01 -0800
  • 657b508cdf fix(tests/lean/simplifier_light): adjust test Leonardo de Moura 2015-12-17 22:42:31 -0800
  • 40b7cf3ad4 chore(frontends/lean): remove unnecessary tokens Leonardo de Moura 2015-12-17 22:35:12 -0800
  • 128b557d37 refactor(frontends/lean): use attribute_manager to simplify decl_attributes Leonardo de Moura 2015-12-17 22:19:55 -0800
  • d81b2d0f29 feat(library/attribute_manager, frontends/lean/builtin_cmds): use attribute manager information when pretty print definitions Leonardo de Moura 2015-12-17 21:16:31 -0800
  • 45dbf76df9 refactor(library): add attribute manager Leonardo de Moura 2015-12-17 20:56:02 -0800
  • 74366aa061 fix(hott): change some theorems to definitions Floris van Doorn 2015-12-17 14:42:30 -0500
  • c852f7bc71 feat(hott): use the induction tactic for trunc at some places Floris van Doorn 2015-12-11 17:13:57 -0500
  • da5f10ce63 feat(hott): minor fixes. allow the usage of numerals for trunc_index Floris van Doorn 2015-12-10 14:37:11 -0500
  • 61ecf018e9 feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ... Leonardo de Moura 2015-12-17 12:18:32 -0800
  • c824a0e050 chore(library,hott): enforce naming conventions Leonardo de Moura 2015-12-17 11:36:35 -0800
  • 13419d1561 chore(hott/library): cleanup Leonardo de Moura 2015-12-17 11:31:07 -0800
  • 2502039a5c fix(frontends/lean/parser): tactic notation that may take numerical parameters Leonardo de Moura 2015-12-17 11:27:31 -0800
  • 70f71a18c8 doc(library/type_context): explain why we need tmp_local_generator Leonardo de Moura 2015-12-15 18:58:07 -0800
  • 73b28c91a6 fix(library/type_context): local constant management bug Leonardo de Moura 2015-12-15 18:49:26 -0800
  • 1387cdfa0f feat(library/type_context): add eta-expansion to type_context Leonardo de Moura 2015-12-15 17:24:53 -0800
  • 10273bf176 feat(library/blast/forward/pattern): improve pattern inference heuristic Leonardo de Moura 2015-12-15 12:55:43 -0800
  • c07345d47f fix(util/file_lock): handle permission denied at lock creation Leonardo de Moura 2015-12-15 09:41:11 -0800
  • 42eda36225 chore(library/algebra/ordered_ring): use 'note' Leonardo de Moura 2015-12-15 09:33:57 -0800
  • ec5990f4de fix(library/norm_num): fix incorrect assert Rob Lewis 2015-12-14 14:09:54 -0500
  • 521657914c chore(util/file_lock): style Leonardo de Moura 2015-12-14 10:20:33 -0800
  • 2185ee7e95 feat(library/tactic): make let tactic transparent, introduce new opaque note tactic Sebastian Ullrich 2015-12-10 19:37:55 +0100
  • 31c9a76777 feat(util/file_lock): add support for Windows Leonardo de Moura 2015-12-14 10:03:33 -0800
  • 95fba3dba6 chore(library/constants): sort constant decls Leonardo de Moura 2015-12-13 21:39:45 -0800
  • 193a9d8cde refactor(library/norm_num): avoid manual constant name initialization Leonardo de Moura 2015-12-13 21:24:31 -0800
  • e3a35ba4fd feat(frontends/lean): add 'with_attributes' tactical Leonardo de Moura 2015-12-13 18:22:51 -0800
  • 727a4f5a3a feat(library/tactic/intros_tactic): use '_' to say that some names are irrelevant in the intro tactic Leonardo de Moura 2015-12-13 16:47:31 -0800
  • d4e49a8434 feat(library/tactic/intros_tactic): intro without argument should introduce a single variable Leonardo de Moura 2015-12-13 16:28:39 -0800
  • 894875dc5c feat(library/tactic/congruence_tactic): closes #855 Leonardo de Moura 2015-12-13 15:03:25 -0800
  • 999f23cbc0 feat(kernel/expr_eq_fn): take names into account when CompareBinderInfo is true Leonardo de Moura 2015-12-13 14:47:11 -0800
  • 49eae56db4 test(library/theories/group_theory): test auto-include in the group theory library Leonardo de Moura 2015-12-13 13:40:54 -0800
  • ce622e9179 feat(frontends/lean): add auto-include for structures and inductive decls Leonardo de Moura 2015-12-13 13:39:34 -0800
  • 20de22a8ad feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included) Leonardo de Moura 2015-12-13 13:20:07 -0800
  • b6bac2e542 chore(tests/lean/run): adjust tests Leonardo de Moura 2015-12-13 12:23:44 -0800
  • 9a4a12899a fix(frontends/lean/pp): make sure pp doesn't group [] arguments Leonardo de Moura 2015-12-13 12:23:22 -0800
  • a9b567296c feat(frontends/lean/parser): add anonymous inst implicit name generator Leonardo de Moura 2015-12-13 11:45:47 -0800
  • ef546c5c5b refactor(library): use anonymous instance implicit arguments Leonardo de Moura 2015-12-13 11:15:10 -0800
  • d26a83da02 feat(frontends/lean/parser): allow anonymous instance implicit arguments Leonardo de Moura 2015-12-13 11:14:12 -0800
  • edad31a9b1 feat(shell/lean): use locking also for the index file Leonardo de Moura 2015-12-12 21:50:08 -0800
  • 4dc3764a02 feat(util,library,shell): basic locking mechanism Leonardo de Moura 2015-12-12 21:16:07 -0800
  • b7de10a6d2 feat(library/trace): allow user to disable subclasses of a trace class Leonardo de Moura 2015-12-11 11:03:16 -0800
  • 7f1800962a feat(frontends/lean/pp): allow user to override pp.all setting Leonardo de Moura 2015-12-11 10:40:48 -0800
  • a35fd06a33 test(tests/lean/run/blast_simp4): add simp test Leonardo de Moura 2015-12-11 10:21:10 -0800
  • ac0bd539b0 feat(frontends/lean/notation_cmd): allow 'abstract ... end' to be used in notation declarations Leonardo de Moura 2015-12-11 09:51:06 -0800
  • eda26a9099 fix(emacs/lean-company): candidate fix for #846 Leonardo de Moura 2015-12-11 08:11:50 -0800
  • 2b1e7e7759 feat(frontends/lean/pp): all disables numerals Daniel Selsam 2015-12-10 17:38:48 -0800
  • abbb2cfbbd feat(library/export): take binder labels into account when max-sharing expression during .olean generation Leonardo de Moura 2015-12-10 23:27:44 -0800
  • 3057dde885 fix(library/class,library/coercion): fixes #852 Leonardo de Moura 2015-12-10 22:46:17 -0800
  • cf61adc5d5 feat(frontends/lean): identifiers starting with '_' are now reserved Leonardo de Moura 2015-12-10 22:32:03 -0800
  • 13f9d8dd6c fix(tests/lean): move hott tests Leonardo de Moura 2015-12-10 10:55:27 -0800
  • 7b29ee1666 fix(library/tactic/induction_tactic): fixes #892 Leonardo de Moura 2015-12-10 10:52:57 -0800
  • 4ef58f1ba5 chore(hott): more cleanup. Floris van Doorn 2015-12-09 17:20:52 -0500
  • c968f920ba chore(hott): cleanup Floris van Doorn 2015-12-09 15:53:48 -0500
  • 8094ca1c70 fix(library/blast/backward): crash when pretty printing backward rule set Leonardo de Moura 2015-12-10 10:38:53 -0800
  • 1abaa9eb71 fix(frontends/lean/parser): fixes #858 Leonardo de Moura 2015-12-10 10:11:23 -0800
  • 8b3cbb8fdd fix(library/tactic/induction_tactic): apply substitution to hypothesis type (it may contain metavars) Leonardo de Moura 2015-12-10 09:49:17 -0800
  • a507ac8594 test(tests/lean/interactive/findp): remove test that breaks whenever we revise init/logic.lean Leonardo de Moura 2015-12-10 09:36:05 -0800
  • c9ff175cf4 fix(library/tactic/induction_tactic): fixes #893 Leonardo de Moura 2015-12-10 09:19:58 -0800
  • 1f8de7b50b feat(library/blast): refine trace messages Leonardo de Moura 2015-12-09 18:38:20 -0800
  • 34e85be970 feat(library/blast): add 'blast.deadend' tracing option Leonardo de Moura 2015-12-09 17:45:36 -0800
  • 1502248d30 feat(library/blast): trace strategy name Leonardo de Moura 2015-12-09 17:13:28 -0800
  • 725101c777 chore(frontends/lean): cleaup Leonardo de Moura 2015-12-09 12:43:06 -0800
  • 65c93b180d fix(types.md): add num Floris van Doorn 2015-12-09 00:17:42 -0500
  • f495fa04c8 fix(tests): fix tests after port Floris van Doorn 2015-12-09 00:11:11 -0500
  • 2325d23f68 feat(hott): port nat and int from the standard library Floris van Doorn 2015-12-09 00:02:05 -0500
  • 46739c8b70 feat(hott/algebra): port abstract structures Floris van Doorn 2015-12-08 12:57:55 -0500
  • 14a2c8e444 fix(init/nat): add spaces around inequalities Floris van Doorn 2015-12-08 11:54:15 -0500
  • 377755e5ab feat(types/sigma): add lemma Floris van Doorn 2015-11-30 19:25:22 -0500
  • 50323e5b14 fix(tests/lean/run/simplifier1): option name Leonardo de Moura 2015-12-09 12:30:20 -0800
  • bed03272f5 fix(tests/lean/run/blast_cc1): option name Leonardo de Moura 2015-12-09 12:23:00 -0800
  • 6abf2fd975 feat(library/blast/congruence_closure): avoid unnecessary propagations in the congruence closure module Leonardo de Moura 2015-12-09 12:17:51 -0800
  • 6bbbc3d50e feat(library/blast): improve trace messages Leonardo de Moura 2015-12-09 11:38:39 -0800
  • a7f5d6603a feat(library/blast/actions/recursor_action): trace recursor name Leonardo de Moura 2015-12-09 11:25:05 -0800
  • 3f9549485f feat(frontends/lean/parser): restore config options in the end of sections/namespaces Leonardo de Moura 2015-12-09 11:24:37 -0800
  • f9a669665a feat(library/blast/backward/backward_action): display lemma name in backward action Leonardo de Moura 2015-12-09 11:07:53 -0800
  • 1b80dc0df6 feat(library/data/real/basic): improve performance Leonardo de Moura 2015-12-09 10:57:16 -0800
  • cbc3c0cf4f feat(frontends/lean): suppress profiling information for declarations that take less than 0.01 secs to be processed Leonardo de Moura 2015-12-09 10:48:36 -0800
  • 0acdcd487b feat(frontends/lean): add 'print aliases' command Leonardo de Moura 2015-12-09 10:39:40 -0800
  • 53a05e845e chore(library/blast/trace): fix style Leonardo de Moura 2015-12-09 09:35:46 -0800