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

Commit graph

  • 87252bbffe fix(library/data/set/basic): add spaces in notation for bounded quantifiers Jeremy Avigad 2016-03-03 11:50:40 -0500
  • dc6cd71236 fix(library/algebra/monotone): fix theorem names Jeremy Avigad 2016-03-02 22:54:51 -0500
  • 4050892889 refactor(library/*): rename 'compose' to 'comp' Jeremy Avigad 2016-03-02 22:48:05 -0500
  • ebb3e60096 feat(library/algebra/monotone): add properties of monotone functions Jeremy Avigad 2016-02-28 21:55:48 -0500
  • 3d09144d73 feat(library/algebra/homomorphism): add homomorphisms between algebraic structures Jeremy Avigad 2016-02-28 09:39:43 -0500
  • 5194df5e97 feat(library/local_context): encode order using a tree instead of a list Leonardo de Moura 2016-03-01 16:23:51 -0800
  • 82fb38b440 feat(util/rb_tree): add for_each_greater Leonardo de Moura 2016-03-01 15:40:22 -0800
  • 2a4b3b75bd refactor(library/blast/state): simplify blast state Leonardo de Moura 2016-03-01 14:27:58 -0800
  • 16dc021736 fix(library/proof_irrel_expr_manager): add missing Let case Leonardo de Moura 2016-03-01 14:27:37 -0800
  • 1104537d02 chore(hott) adjust to new naming for pointed types and truncated types Jakob von Raumer 2016-03-01 13:00:12 +0000
  • 2b13777bbe feat(hott) add type functors, maybe they should be changed to be un-funexted. Jakob von Raumer 2016-02-26 15:54:56 +0000
  • 11458f64fe feat(hott/algebra) add order categories Jakob von Raumer 2016-02-26 14:10:54 +0000
  • 4e67a35179 feat(library/blast/blast): add missing Let case, and comment to indicate performance problem Leonardo de Moura 2016-03-01 13:47:43 -0800
  • c23528b5d8 feat(library/blast/blast): use defeq_simplifier to normalize Daniel Selsam 2016-02-26 21:10:13 -0800
  • 20e7ff39cc feat(library/proof_irrel_expr_manager): eq and hash modulo proof irrelevance Daniel Selsam 2016-02-25 19:13:33 -0800
  • a9c6bce7cc feat(library/defeq_simplifier): some generic normalization Daniel Selsam 2016-02-25 18:57:26 -0800
  • 2982db6f80 feat(library/local_context): add new local context type Leonardo de Moura 2016-03-01 13:32:19 -0800
  • f3648e2ac8 refactor(library/blast/blast): remove old hack Leonardo de Moura 2016-03-01 12:24:24 -0800
  • 56d7fc4c23 refactor(*): cleanup replace_visitor subclasses, and make sure let-expressions are handled Leonardo de Moura 2016-02-29 16:55:19 -0800
  • 3c878ecd01 feat(kernel): add let-expressions to the kernel Leonardo de Moura 2016-02-29 16:40:17 -0800
  • f55e456c84 chore(*): remove remaining references to by+ and begin+ Leonardo de Moura 2016-02-29 13:59:06 -0800
  • b7b4b6d838 chore(src/frontends/lean/builtin_exprs): remove unnecessary parameter Leonardo de Moura 2016-02-29 13:53:57 -0800
  • f54963bc3e refactor(library/tactic/expr_to_tactic): remove 'by_plus' support Leonardo de Moura 2016-02-29 13:50:05 -0800
  • fbe5188480 refactor(frontends/lean): remove 'by+' and 'begin+' tokens Leonardo de Moura 2016-02-29 13:45:43 -0800
  • 79ba2638b7 fix(library/data/set/equinumerosity): add missing 'using' Leonardo de Moura 2016-02-29 13:29:03 -0800
  • bf60999ede fix(frontends/lean/builtin_exprs): 'using' expression Leonardo de Moura 2016-02-29 13:23:39 -0800
  • faa0031d4e refactor(library,hott): remove 'by+' and 'begin+' Leonardo de Moura 2016-02-29 13:15:48 -0800
  • 15c4bc92b9 refactor(frontends/lean/elaborator): we only need to track one context Leonardo de Moura 2016-02-29 12:49:17 -0800
  • 2b1d734544 feat(kernel/expr): remove 'contextual' flag from binder_info Leonardo de Moura 2016-02-29 12:41:43 -0800
  • b41c65f549 feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking Leonardo de Moura 2016-02-29 12:31:23 -0800
  • 3b73b5b207 fix(library/theories/group_theory): have-tactic Leonardo de Moura 2016-02-29 12:13:53 -0800
  • cc8d9bc7ff refactor(hott): replace 'assert'-expr with 'have'-expr Leonardo de Moura 2016-02-29 12:11:17 -0800
  • deb1b3dc79 refactor(library): replace assert-exprs with have-exprs Leonardo de Moura 2016-02-29 11:47:33 -0800
  • 101cf1ec4c feat(frontends/lean): remove difference between 'have' and 'assert' Leonardo de Moura 2016-02-29 11:28:20 -0800
  • 23079a75a7 dev(lp): fix build for clang, avoid clang-3.3 bug, cleanup permutation_matrix Lev Nachmanson 2016-02-24 13:52:31 -0800
  • 2fd5347901 refactor(library/blast): ppb is not necessary anymore Leonardo de Moura 2016-02-26 15:51:46 -0800
  • eee74ef1b4 refactor(frontends/lean/pp): use abstract_type_context instead of type_checker Leonardo de Moura 2016-02-26 15:35:29 -0800
  • 7d61f640f6 refactor(*): add abstract_type_context class Leonardo de Moura 2016-02-26 14:17:34 -0800
  • 5a4dd3f237 feat(library/reducible): remove [quasireducible] annotation Leonardo de Moura 2016-02-25 17:42:44 -0800
  • d501295ec1 refactor(algebra/binary): remove unnecessary annotations Leonardo de Moura 2016-02-25 15:11:52 -0800
  • 768ba1c363 refactor(library/hott): remove more unnecessary annotations Leonardo de Moura 2016-02-25 14:30:00 -0800
  • 510168a387 refactor(library,hott): remove unnecessary annotations Leonardo de Moura 2016-02-25 12:26:20 -0800
  • 146edde5b3 feat(library/class): mark instances as quasireducible by default Leonardo de Moura 2016-02-25 12:10:07 -0800
  • c85d6d5a1e fix(library/init/tactic): typo Leonardo de Moura 2016-02-24 16:10:35 -0800
  • 1924b2884c refactor(library/tactic): remove 'append' and 'interleave' tacticals Leonardo de Moura 2016-02-24 15:53:50 -0800
  • 9b15c4c669 feat(util/rb_map): add find_if Leonardo de Moura 2016-02-24 15:30:25 -0800
  • f38af35e06 fix(script/check_md_links.py): author name Soonho Kong 2016-02-23 20:17:03 -0500
  • e6895e3619 chore(script/check_md_links.py): add copyright Soonho Kong 2016-02-23 18:03:15 -0500
  • ff1352fcf2 fix(script/check_md_links.py): import print_function from __future__ Soonho Kong 2016-02-23 18:02:44 -0500
  • 596fe17f16 feat(script/check_md_links.py): make python2/3 compatible Soonho Kong 2016-02-23 14:33:16 -0500
  • 494b88e103 fix(library/blast/forward/ematch): must used the right type_context Leonardo de Moura 2016-02-23 13:32:34 -0800
  • 2a35c0f49b feat(script): add .md link checker script Sebastian Ullrich 2016-02-23 14:23:47 +0100
  • 3de216d302 chore(*.md): fix/remove broken links Sebastian Ullrich 2016-02-23 01:41:22 +0100
  • 2a294bcc17 fix(frontends/lean/elaborator): fixes #996 Leonardo de Moura 2016-02-22 17:03:14 -0800
  • 96f391dda2 feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command Leonardo de Moura 2016-02-22 16:01:12 -0800
  • 49661a043d feat(library/definitional/equations): improve detection of infeasible cases in the definitional package Leonardo de Moura 2016-02-22 14:05:28 -0800
  • 431ce6ff2d fix(util/lp): instantiate missing functions Soonho Kong 2016-02-22 16:16:37 -0500
  • 1546c04154 feat(library/theories/analysis/complex_norm): instantiate complex numbers as a real normed vector space Jeremy Avigad 2016-02-20 13:17:10 -0500
  • 5246072e96 feat(library/theories/analysis/inner_product): add real inner product spaces Jeremy Avigad 2016-02-20 10:47:05 -0500
  • 7f1eb76091 feat(library/theories/analysis/normed_space): add specializations to modules over the reals, to help the elaborator Jeremy Avigad 2016-02-20 10:45:07 -0500
  • ea42a76dc5 refactor/feat(library/theories/analysis/sqrt): break out sqrt, add properties Jeremy Avigad 2016-02-20 10:23:41 -0500
  • 3c18f05cab feat(library/algebra): add some useful facts Jeremy Avigad 2016-02-20 08:27:59 -0500
  • 0f81c2e65b fix(tests/lean/noncomp_theory,simlifier_light): fix tests Jeremy Avigad 2016-02-16 22:00:29 -0500
  • 158acf878d feat(library/data/set/filter): work in material from Jacob Gross Jeremy Avigad 2016-02-16 21:57:10 -0500
  • 41342f53df refactor(library/data/set/filter): get filters working with complete lattice notation Jeremy Avigad 2016-02-16 17:29:52 -0500
  • a08395b17e refactor(library/algebra/complete_lattice): make complete lattices more usable Jeremy Avigad 2016-02-16 17:26:11 -0500
  • 7fe71c972f feat(library/data/set/basic): add theorems for bounded unions and intersections Jeremy Avigad 2016-02-16 17:24:55 -0500
  • 518a77587a refactor(library/data/{set,finset},library/*): use compl for set and finset complement Jeremy Avigad 2016-02-16 13:56:01 -0500
  • 8f83c78bc9 fix(library/logic/identities,library/*): fix implicit arguments, add implications. Closes #1002. Jeremy Avigad 2016-02-16 11:54:26 -0500
  • 769ae6830d feat(library/data/set/function): add facts about preimages Jeremy Avigad 2016-02-16 09:07:12 -0500
  • a72f6666e8 feat(library/data/set/basic): add two theorems Jeremy Avigad 2016-02-16 08:00:47 -0500
  • 797905b803 feat(library/theories/topology/order_topology): add order_topology, from Jacob Gross Jeremy Avigad 2016-02-15 22:23:29 -0500
  • b8d3f34d14 feat(library/data/set/basic): add a couple of theorems Jeremy Avigad 2016-02-15 22:13:34 -0500
  • 03cd2c0013 feat/refactor(library/algebra/interval): use i for infinite, add some theorems Jeremy Avigad 2016-02-15 22:07:41 -0500
  • e80559237a fix(library/data/real): tinker with instances Jeremy Avigad 2016-02-14 18:03:57 -0500
  • 15c9ec12cf fix(library/data/real/division): make temporary has_div only a local instance Jeremy Avigad 2016-02-14 10:16:13 -0500
  • 6cdbc0f79f feat(pointed/equiv): add more theorems Floris van Doorn 2016-02-17 11:41:31 -0500
  • eea2a1ac91 feat(hott): add some more abstracts Floris van Doorn 2016-02-16 18:25:40 -0500
  • b2181497fd fix(tests): fix delta_issue2 Floris van Doorn 2016-02-16 12:29:58 -0500
  • facd94a1b4 feat(hott): various changes Floris van Doorn 2016-02-15 20:59:38 -0500
  • 087c44d614 style(hott): rename instances of pType using pfoo instead of Foo Floris van Doorn 2016-02-15 18:23:28 -0500
  • c64e5a114c feat(circle): add missing facts that the circle is 1-truncated and 0-connected Floris van Doorn 2016-02-15 16:24:24 -0500
  • bac6d99cc7 style(hott): rename Pointed to pType Floris van Doorn 2016-02-15 16:05:31 -0500
  • 43cf2ad23d style(hott): replace all other occurrences of hprop/hset Floris van Doorn 2016-02-15 15:55:29 -0500
  • 4e2cc66061 style(*): rename is_hprop/is_hset to is_prop/is_set Floris van Doorn 2016-02-15 15:18:07 -0500
  • 816237315c feat(hott): various additions, especially for pointed maps/homotopies/equivalences Floris van Doorn 2016-02-15 14:40:25 -0500
  • ecc141779a feat(init.path): update init.path to use tactics, also some additions Floris van Doorn 2016-02-15 12:57:51 -0500
  • 7f09ba328e feat(hott): small changes Floris van Doorn 2016-02-13 00:12:13 -0500
  • 78092af27f feat(hott): add some attributes Floris van Doorn 2016-02-11 17:58:19 -0500
  • cd74b6bff0 fix(hott): abstract some equivalence proofs Floris van Doorn 2016-02-11 13:58:31 -0500
  • db8ed5dd08 feat (library/theories/topology/basic) : add separation theorems Jacob Gross 2016-02-14 13:23:08 -0500
  • 7852524370 fix(library/data/list/sorted): incorrect name Sean Leather 2016-02-14 16:34:03 +0200
  • 859a3d35ea feat(library/defeq_simplifier): no need to reverse args Daniel Selsam 2016-02-13 14:21:08 -0800
  • d521063dfb feat(library/defeq_simplifier): new simplifier that uses only definitional equalities Daniel Selsam 2016-02-13 10:52:25 -0800
  • 20f70035dd fix(frontends/lean/util): fixes #1007 Leonardo de Moura 2016-02-22 10:44:22 -0800
  • 994815bc77 fix(bin/linja.in): roll back d8fb6f5 Soonho Kong 2016-02-15 14:31:15 -0500
  • ca1901bb2c feat(emacs/lean-project.el): ask 'project type' in lean-project-create Soonho Kong 2016-02-12 22:02:24 -0500
  • b047c9c037 refactor(theories/{analysis, topology}): clean up proofs connecting open balls and open sets Rob Lewis 2016-02-10 13:44:16 -0500
  • 68bc41b5fe feat(data/set): add missing set theorems Rob Lewis 2016-02-10 13:40:47 -0500
  • 4a41e78124 fix(theories/analysis): make variables implicit in continuous_at_intro Rob Lewis 2016-02-09 19:10:49 -0500