Commit graph

Select branches

Hide pull requests

imp_hott

master

mzhang/fix

#1

#10

#13

#13

#2

#3

#3

#4

#4

#8

Mono Color

• 6f25abfb87 feat(library/algebra): missing theorems Rob Lewis 2016-05-25 15:31:44 -0400
• 670ee10b27 feat(library/analysis): basic properties about real derivatives Rob Lewis 2016-04-20 14:31:07 -0400
• 92531fba16 feat(theories/analysis): intro/elim rules for continuous_on, etc Rob Lewis 2016-04-19 18:17:53 -0400
• 963c9e8977 feat(theories/topology): add missing continuity facts Rob Lewis 2016-04-19 18:17:15 -0400
• 194cd89000 feat(theories/analysis): use new homomorphism names from algebra Rob Lewis 2016-04-18 17:02:27 -0400
• 89de67f4c3 feat(algebra/ordered_field): add missing theorems about division Rob Lewis 2016-04-18 13:45:37 -0400
• 3482e1eab9 feat(theories/analysis): finish basic properties of Frechet derivative Rob Lewis 2016-04-18 13:45:05 -0400
• 99a4ffb8f2 feat(theories/analysis): more on frechet derivatives Rob Lewis 2016-02-19 12:32:19 -0500
• 3c0f19c967 feat(theories/analysis): define frechet derivative + basic theorems Rob Lewis 2016-02-17 13:48:50 -0500
• c87e79ff7f feat(theories/analysis): add weak squeeze theorem for converges_to_at Rob Lewis 2016-02-17 13:48:19 -0500
• 56ca41a916 feat(algebra/module): difference of linear operators is linear Rob Lewis 2016-02-17 13:46:53 -0500
• 79ff2f7b8f feat(algebra/ordered_field): add stronger division sign theorem Rob Lewis 2016-02-17 13:40:19 -0500
• 47843e4fe1 refactor(README.md): change Latex link from pygments to lstlean Jeremy Avigad 2016-05-24 21:32:29 +0200
• 2bc67cf936 refactor(library/theories/analysis/metric_space): refactor some proofs Jeremy Avigad 2016-05-19 11:38:32 -0400
• e17c5c4f08 feat(library/theories/analysis/*): install new limits Jeremy Avigad 2016-05-18 21:21:49 -0400
• dd8be61c84 feat(library/theories/topology/limit): add general properties of limits, various improvements Jeremy Avigad 2016-05-18 12:10:38 -0400
• eae80118bf feat(library/theories/topology/limit.lean): add topological filters Jeremy Avigad 2016-05-16 09:40:20 -0400
• b8c230a55d refactor(library/theories/topology/approaches): rename 'filterlim' to 'tendsto' etc., and general cleaning Jeremy Avigad 2016-05-13 18:23:09 -0400
• 057935d844 fix(emacs): set pp.width to column width instead of buffer width of flycheck error list Sebastian Ullrich 2016-05-29 23:04:34 -0400
• 9fa30e3f7d chore(emacs): remove Lua support Sebastian Ullrich 2016-05-11 13:50:45 -0400
• 66ec690061 feat(book): add new theorems to book.md Floris van Doorn 2016-04-25 20:08:28 -0400
• 52dd6cf90b feat(hott): Port files from other repositories to the HoTT library. Floris van Doorn 2016-04-22 15:12:25 -0400
• ab7adf3084 fix(pathover): remove unused argument of loop_pathover Floris van Doorn 2016-04-21 15:42:11 -0400
• 2afdaf6906 fix(groupoid): redefine groupoid given by a group Floris van Doorn 2016-04-22 19:11:22 -0400
• 1135d80266 feat(hott): use group isomorphisms instead of equality between groups Floris van Doorn 2016-04-20 11:51:56 -0400
• 8db4676c46 feat(hott): various changes and additions in the HoTT library Floris van Doorn 2016-04-11 13:11:59 -0400
• a6b5191be6 feat(pushout/susp): change definition of elim_type, so that flattening is easier to prove Floris van Doorn 2016-04-14 17:09:38 -0400
• c6726d22ec doc(export_format): minor fixes Daniel Selsam 2016-05-05 08:49:45 -0700
• e6fd644526 feat(library/theories/group_theory/*): add new development of group theory Jeremy Avigad 2016-05-05 19:53:03 -0400
• f8a8502b14 refactor(library/theories/group_theory): rename group_theory to finite_group_theory Jeremy Avigad 2016-05-05 19:18:25 -0400
• ef95a04d21 chore(README.md): add link to Emacs mode information. Closes #1046. Jeremy Avigad 2016-05-05 19:16:34 -0400
• d773302c6b chore(doc/lean/tutorial.org): comment out old rewriter information Jeremy Avigad 2016-05-05 19:13:28 -0400
• b02009fcb9 feat(src/emacs/README.md): add more information about key bindings and commands Jeremy Avigad 2016-04-29 17:14:09 -0400
• 2ef22fceca fix(util/lp/lp_solver.h): get_max_iterations_per_stage returns unsigned Soonho Kong 2016-05-06 11:36:40 -0400
• 4eee26eaee feat(library/data/sigma): add imp_sigma Sean Leather 2016-03-21 12:07:22 +0200
• 933b5863cd fix(tests/lean/770): adjust test output Leonardo de Moura 2016-04-11 09:50:46 -0700
• eeee7d51cf chore(kernel/error_msgs): show inferred type when function expected Daniel Selsam 2016-04-02 14:55:17 -0700
• e721cf9c79 refactor(algebra/matrix): rename theorems, split proof of transposition theorem Rob Lewis 2016-03-24 15:45:33 -0400
• 85f8f7df57 feat(algebra/matrix): reorganize file; generalize Farkas' lemma to Motzkin transposition theorem Rob Lewis 2016-03-23 13:26:33 -0400
• 5a640590cc feat(data/{list,fin}): add theorems for use in matrices Rob Lewis 2016-03-23 13:25:42 -0400
• 66cd4f1196 feat(algebra/matrix): generalize theorems, define module/ring instances Rob Lewis 2016-03-20 17:15:49 -0400
• b7a25a249a feat(library/algebra): define matrices, prove Farkas' lemma Rob Lewis 2016-03-17 17:29:55 -0400
• 651df51cb7 chore(hott) the coercion doesn't seem to be the problem Jakob von Raumer 2016-03-30 13:59:55 +0100
• 7a9e1c7f4f chore(hott) fix sum proof by adding manual coercions Jakob von Raumer 2016-03-30 11:43:41 +0100
• a6319118e3 feat(types.pointed): small additions Floris van Doorn 2016-03-29 15:41:28 -0400
• f983724cf6 feat(pointed): merge pointed2 into pointed Floris van Doorn 2016-03-28 16:33:33 -0400
• 4895726c54 feat(connectedness): show that if f is n-connected, then trunc_functor k f is so, too Floris van Doorn 2016-03-28 12:46:17 -0400
• 54da5bcbda feat(hott): add some [constructor] attributes Floris van Doorn 2016-03-24 17:28:29 -0400
• 3887efa7c1 feat(hott): some renamings in init.path Floris van Doorn 2016-03-19 12:09:44 -0400
• 3240df6020 feat(book): add comments about chapter 10 Floris van Doorn 2016-03-19 17:46:53 -0400
• dc37ec954d refactor(hott): rename apdo to apd Floris van Doorn 2016-03-19 11:25:08 -0400
• 80a2e285cb feat(init/ua): add ua_symm and ua_trans Floris van Doorn 2016-03-19 11:10:33 -0400
• 05b59aecf8 refactor(hott): rename apd to apdt Floris van Doorn 2016-03-19 10:38:05 -0400
• b1ed69f621 feat(hott): small changes, mostly in pointed2 Floris van Doorn 2016-03-08 00:16:45 -0500
• 5810a4de8f fix(emacs/lean-server.el): invoke lean --server from project root if existent Sebastian Ullrich 2016-04-08 23:38:45 +0200
• 08c55754a9 fix(emacs/lean-mode.el): invoke lean from project root if existent Sebastian Ullrich 2016-04-06 20:48:52 +0200
• 543d7702f0 fix(shell/lean): fix documentation of some cmdline options Sebastian Ullrich 2016-04-06 20:50:36 +0200
• 1f967695a8 feat(library/theories/measure_theory/sigma_algebra): add measurable and borel functions, from Jacob Gross Jeremy Avigad 2016-04-06 17:44:09 -0400
• ef982d9ad6 refactor(library/theories/analysis/metric_space.lean): use new definition of continuous_at Jeremy Avigad 2016-04-06 16:44:29 -0400
• c0720d69e3 feat(library/theories/topology/continuous.lean): add theorems about continuous functions (includes work by Jacob Gross) Jeremy Avigad 2016-04-06 16:24:12 -0400
• 73271ac2c9 feat(library/theories/move.lean): add facts to move in Lean 3 Jeremy Avigad 2016-04-06 16:14:14 -0400
• 226f8bafeb fix(library/tactic/rewrite_tactic): do not allow projections to be unfolded Leonardo de Moura 2016-03-28 12:53:49 -0700
• a07ad6df62 fix(library/tmp_type_context): fixes #1033 Leonardo de Moura 2016-03-28 09:38:22 -0700
• 6f74f65220 fix(library/type_context): instantiate was not replacing all assigned metavars Leonardo de Moura 2016-03-23 13:37:33 -0700
• 1c52062f1e chore(hott): standardize names of homotopy_of_inv_homotopy_post and friends Ulrik Buchholtz 2016-03-14 19:11:21 -0400
• 5257e282aa feat(hott/homotopy): additions to sphere and susp, improve quaternionc_hopf Ulrik Buchholtz 2016-03-10 19:53:42 -0500
• 7e8ba1440f feat(hott): update book.md and homotopy.md to reflect additions Ulrik Buchholtz 2016-03-06 20:03:27 -0500
• f11169b8f2 feat(hott): the quaternionic hopf fibration Ulrik Buchholtz 2016-03-06 19:41:58 -0500
• 89296ec52a feat(hott): the complex hopf fibration S3 to S2 Ulrik Buchholtz 2016-03-06 18:09:32 -0500
• d53320cb0f feat(hott): the imaginaroid version of the cayley dickson construction Ulrik Buchholtz 2016-03-06 15:44:49 -0500
• 0b9084c7d2 feat(hott): hopf construction and delooping of K(G,1)s Ulrik Buchholtz 2016-03-06 15:34:44 -0500
• bb64913e50 feat(hott): flattening lemma for susp Ulrik Buchholtz 2016-03-06 13:59:48 -0500
• bd9e47c82c feat(hott): functoriality of pushout; connectedness in is_conn namespace Ulrik Buchholtz 2016-02-08 12:07:53 +0100
• a8db8bc61a feat(library/theories/topology/filterlim): add general theory of limits, based on filters Jeremy Avigad 2016-03-09 13:36:48 -0500
• 8f0a0d2b32 feat(library/export, doc/export_format): remove support for mutually inductive types Daniel Selsam 2016-03-10 20:07:09 -0800
• 0c4a6d3c5e chore(data/set): cleanup proofs to make them less dependent on unifier heuristics Leonardo de Moura 2016-03-09 18:46:23 -0800
• 5e14b4ebe8 fix(library,hott): avoid rewrite with patterns of the form (?M ...) Leonardo de Moura 2016-03-09 14:21:33 -0800
• d4f0ce0eab fix(library/local_context): typo Leonardo de Moura 2016-03-09 13:59:21 -0800
• 003c11c917 feat(connectedness): is_conn_map -> is_conn_fun, and unbundle the P in elimination principles Floris van Doorn 2016-03-06 11:24:59 -0500
• 1e10810a1e feat(init/funext): add function extensionality as an axiom. Floris van Doorn 2016-03-06 11:24:07 -0500
• 2d9c3985c9 feat(square): add variants of eq_pathover Floris van Doorn 2016-03-06 10:59:00 -0500
• 671ef077b9 feat(hott): additions, mostly to types.trunc Floris van Doorn 2016-03-05 19:35:12 -0500
• ea775092bb fix(tests): use have instead of assert Floris van Doorn 2016-03-03 13:00:38 -0500
• c50ab524a5 fix(emacs/lean-project.el): update prompt message, have standard as a defualt Soonho Kong 2016-03-04 15:18:45 -0500
• 7e64405f5e fix(emacs/lean-project.el): check project-type argument Soonho Kong 2016-03-04 12:07:24 -0500
• 5cacebcf86 feat(hott): replace assert by have and merge namespace equiv.ops into equiv Floris van Doorn 2016-03-03 10:48:27 -0500
• 058000f61d feat(homotopy/homotopy_group): add theorems in section 8.3 of the HoTT book Floris van Doorn 2016-03-02 18:36:46 -0500
• 1903601ba5 refactor(trunc): rename namespace is_trunc.trunc_index to trunc_index Floris van Doorn 2016-03-02 17:19:44 -0500
• e2b31a9b33 feat(hott): remove multiple_instances attribute Floris van Doorn 2016-03-02 16:50:20 -0500
• af4ba3d2fb feat(hott): prove that the (n+1)-sphere is n-connected Floris van Doorn 2016-03-02 16:23:24 -0500
• e515875464 feat(hott): various additions Floris van Doorn 2016-02-29 23:37:03 -0500
• c6e628da12 feat(hott): more computation rules for trunc_index and use nats for Lemma 8.6.2 Floris van Doorn 2016-02-26 17:00:28 -0500
• e5d5ef9d55 feat(hott/library): various changes and additions. Floris van Doorn 2016-02-24 19:43:50 -0500
• 65b367ddff feat(fin): port more parts of fin from the standard library Floris van Doorn 2016-02-23 16:23:46 -0500
• bf403e124a feat(nat/div): port to HoTT library Floris van Doorn 2016-02-23 16:01:34 -0500
• 4238fdd3d8 fix(hott): add missing links to markdown files Floris van Doorn 2016-02-23 13:00:16 -0500
• d84a20d68b remove(frontends/lean/server): FINDG command Leonardo de Moura 2016-03-01 19:41:46 -0800
• 22f3efc5be remove(frontends/lean): begin_end pre-tactics Leonardo de Moura 2016-03-01 19:30:57 -0800
• d54a67cf2e fix(library): compilation warnings on OSX Leonardo de Moura 2016-03-01 17:50:28 -0800
• 6f766dd33e chore(library/blast): cleanup Leonardo de Moura 2016-03-01 17:42:57 -0800