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

Commit graph

  • bb67a3b9bf feat(hott/algebra/homomorphism): more general treatment of homomorphisms Jeremy Avigad 2017-01-11 13:45:42 -0500
  • 4d4a0c7c53 chore(tests/lean/run/num_norm1): remove test for broken tactic Leonardo de Moura 2016-12-30 13:59:58 -0800
  • e0f1b16604 chore(library): minor library changes Sebastian Ullrich 2016-12-10 22:21:33 +0100
  • 98fa04b1ff fix(bin/linja): fix some file name escaping Sebastian Ullrich 2016-12-10 21:56:42 +0100
  • 3e3ce6b8ca feat(util/name): accept more subscripts in identifiers Sebastian Ullrich 2016-12-10 21:55:53 +0100
  • d7320f4938 fix(frontends/lean): fix some output of escaped identifiers Sebastian Ullrich 2016-08-25 10:08:40 -0400
  • a086fb3348 chore(tests/lean/interactive): remove broken old tests Leonardo de Moura 2016-11-29 14:34:39 -0800
  • e87a27cb4b fix(hott/init/path): reorder arguments of whisker_right Floris van Doorn 2016-11-24 00:13:05 -0500
  • a9fc853985 feat(hott/homotopy/EM): redefine Eilenberg-Maclane spaces and prove their uniqueness Floris van Doorn 2016-11-23 23:07:59 -0500
  • 4ed4fb7c67 feat(hott/homotopy): cleanup cofiber and wedge, redefine smash Floris van Doorn 2016-11-23 21:36:25 -0500
  • 9342fe2716 feat(hott) move many lemmas to library, and cleanup various parts Floris van Doorn 2016-11-23 17:59:13 -0500
  • ecbe4af3c7 fix(hott:group): use only reducible definitions in instances Floris van Doorn 2016-11-14 17:06:48 -0500
  • d12a2a264b fix(hott:group_theory): change group to has_mul Floris van Doorn 2016-11-10 17:25:20 -0500
  • 242f6b8743 fix(README): links Leonardo de Moura 2016-12-01 13:29:29 -0800
  • 94c007868f chore(README): update Leonardo de Moura 2016-12-01 13:28:19 -0800
  • 7596ea285e fix(doc/lean/tutorial): correct some typos and infelicities in the short tutorial Ramana Kumar 2016-10-31 11:47:28 +1100
  • 82f71e4561 fix(library/blast/congruence_closure): fix what look to be typos in congr_key_cmp Ramana Kumar 2016-10-31 10:59:43 +1100
  • 97a6fc23aa chore(emacs): input & highlighting Sebastian Ullrich 2016-08-26 17:26:29 -0400
  • 7ece6ca3a8 fear(frontends/lean): pretty-printing Sebastian Ullrich 2016-08-26 17:26:11 -0400
  • 692b358031 feat(frontends/lean/scanner): accept arbitrary escaped identifiers Sebastian Ullrich 2016-08-25 10:08:40 -0400
  • 9f8eef5e65 feat(emacs): integrate lean-next-error-mode Sebastian Ullrich 2016-08-04 14:00:55 -0400
  • 2014b86cf7 fix(library/tc_multigraph): remove incorrect assertion Leonardo de Moura 2016-09-29 01:35:05 -0700
  • 70a5f98747 fix(tests): fix crash1 Floris van Doorn 2016-09-22 18:47:47 -0400
  • d5a72f6327 feat(homotopy_group): use is_succ for homotopy groups Floris van Doorn 2016-09-22 16:00:14 -0400
  • 341a53b880 feat(pointed): make the naming in the pointed library more consistent. Floris van Doorn 2016-09-22 15:42:46 -0400
  • 554abe88c2 feat(hott/algebra): define bundled additive groups as multiplicative groups Floris van Doorn 2016-09-19 22:13:16 -0400
  • c884e7bbb9 feat(hott/algebra): define additive structures to be multiplicative structures Floris van Doorn 2016-09-19 14:41:21 -0400
  • 8d6010ccad feat(pointed): use pointed equivalences instead of equalities for some lemmas Floris van Doorn 2016-09-18 01:44:19 -0400
  • e2734080c6 fix(algebra): change the reducibility of some defintions Floris van Doorn 2016-09-18 00:14:19 -0400
  • 11c08c51e6 fix(algebra/group_theory): split homomorphisms into additive and multiplicative homomorphisms Floris van Doorn 2016-09-17 19:26:03 -0400
  • c68e013fcb refactor(fin+nat): move is_succ to nat Floris van Doorn 2016-09-17 19:08:41 -0400
  • d70334d100 feat(hott/algebra/bundled): add a parameter to Group to specify whether it's an additive or multiplicative group Floris van Doorn 2016-09-17 18:37:49 -0400
  • 467001c0a9 feat(hott): minor changes Floris van Doorn 2016-07-13 09:39:16 +0100
  • ddec6f77ee feat(category.pushout): finish second way of formulating universal property Floris van Doorn 2016-07-12 09:51:00 +0100
  • fd5adb831b feat(category.pushout): finish universal property of pushout Floris van Doorn 2016-06-28 16:34:11 +0100
  • fe1fbae540 feat(category.pushout): give the universal property of the pushout of categories Floris van Doorn 2016-06-24 15:03:47 +0100
  • c81c86a9b8 chore(hott) remove duplicate lemma, make defs private, update book.md Jakob von Raumer 2016-08-04 17:33:25 +0200
  • e79063970d feat(hott) finish proof of lemma 9.9.4 Jakob von Raumer 2016-08-04 14:58:45 +0200
  • 5f06496f89 feat(hott) almost finish 9.9.4 proof Jakob von Raumer 2016-07-27 13:23:42 +0200
  • 3e1ee4b714 feat(hott) add functor axioms for lemma 9.9.4 construction Jakob von Raumer 2016-07-26 23:41:29 +0200
  • d26d98531c feat(hott) add morphism part of construction for lemma 9.9.4 Jakob von Raumer 2016-07-25 18:41:42 +0200
  • 8718a649c4 feat(hott) add first bit of proof of 9.9.4: construction of some gadgets and prove that they are contractible Jakob von Raumer 2016-07-20 16:03:01 +0200
  • 143bd765f3 chore(hott) fix markup syntax in book.md Jakob von Raumer 2016-07-18 17:27:54 +0200
  • 3416430cfa chore(hott) update book.md Jakob von Raumer 2016-07-18 17:25:59 +0200
  • 548671ce1b feat(hott) prove lemma 9.9.2: essentially surjective and full functors induce fully faithful functors in the functor category Jakob von Raumer 2016-07-18 17:10:32 +0200
  • 0ff8a96be1 feat(hott) formalize book lemma 9.9.1: essentially surjective functors induce faithful functors in the functor category Jakob von Raumer 2016-07-15 18:20:42 +0200
  • 3de39200a4 chore(hott) update book.md and constructions.md to include rezk completion Jakob von Raumer 2016-07-05 15:57:19 +0200
  • 2cdefbbf0c feat(library/theories/commutative_algebra/ideal.lean): add ideals and ring quotient Jeremy Avigad 2016-07-27 14:19:57 -0400
  • e72032d46a fix(library/theories/group_theory/{basic,quotient}): small fixes Jeremy Avigad 2016-07-27 12:46:14 -0400
  • cc70845332 chore(hott) update book.md and constructions.md to include rezk completion Jakob von Raumer 2016-07-05 15:57:19 +0200
  • 18a27cf963 chore(hott) merge namespaces in rezk completion Jakob von Raumer 2016-07-05 15:56:47 +0200
  • 82a8d137da feat(hott) prove that rezk functor is a weak equivalence Jakob von Raumer 2016-07-02 17:40:36 +0200
  • 57bf0a09dd feat(hott) add rezk completion as univalent category Jakob von Raumer 2016-07-02 14:49:05 +0200
  • 86d9a1c84d feat(hott) add id_of_iso of rezk completion Jakob von Raumer 2016-07-01 19:35:13 +0200
  • 6d6ab3f36b feat(hott) instantiate rezk completion as precategory Jakob von Raumer 2016-06-30 14:54:33 +0200
  • 64e1e5404c feat(hott) add composition for rezk completion Jakob von Raumer 2016-06-30 13:45:29 +0200
  • 5c4aac6c8a feat(hott) add idenity for rezk completion Jakob von Raumer 2016-06-30 01:26:56 +0200
  • 8d4ad591c8 feat(hott) add missing pathover lemmas Jakob von Raumer 2016-06-27 17:19:54 +0200
  • a5fe82f177 feat(hott) add carrier and hom set of rezk completion Jakob von Raumer 2016-06-24 02:22:10 +0200
  • a5fb28ca78 chore(frontends/lean,tests): fix tests and style Leonardo de Moura 2016-07-09 10:29:34 -0700
  • 53236718a8 refactor(library/data/pnat): make pnat a decidable_linear_order Gabriel Ebner 2016-06-17 12:03:31 +0200
  • e4071639f1 fix(builtin_cmds): metavar_args should be false by default Floris van Doorn 2016-06-06 12:55:12 -0400
  • 2cc8914874 feat(homotopy): add results about infty-connectedness and loops of EM-spaces Floris van Doorn 2016-06-24 09:54:00 +0100
  • 3213b1b3b0 feat(EM): Prove some corollaries of Whitehead's principle, and prove that K(G,1) is unique. Floris van Doorn 2016-06-23 23:38:35 +0100
  • fb81bcaeee fix(tests): fix tests after changes is the HoTT library Floris van Doorn 2016-06-23 23:26:37 +0100
  • 17ccc283a9 feat(hott): move basic theorems from colimit development to library. Floris van Doorn 2016-06-23 21:49:54 +0100
  • ae1b2e854c feat(hott): various minor changes Floris van Doorn 2016-06-23 21:10:37 +0100
  • fcf06ae2f5 feat(vankampen): prove the van Kampen theorem with basepoints Floris van Doorn 2016-06-23 21:09:18 +0100
  • e5ab514263 feat(lstlean.tex): add Omega, and fix ` and * Floris van Doorn 2016-06-23 11:54:29 +0100
  • 15cdd593c1 feat(init.{equiv|ua}): remove duplicated theorem Floris van Doorn 2016-05-30 14:24:15 -0400
  • 41de1a8271 feat(hit): add construction of propositional truncation to the library Floris van Doorn 2016-05-20 17:07:45 -0400
  • 735230ad07 feat(hott): small changes, simplify van Kampen Floris van Doorn 2016-05-19 11:27:52 -0400
  • e96e4a677d feat(homotopy): prove the naive Seifert-Van Kampen theorem Floris van Doorn 2016-05-18 00:33:35 -0400
  • 61848c4a2e feat(hott): define pushout of groupoids Floris van Doorn 2016-05-17 22:36:16 -0400
  • 9f13527c25 chore(hott): update default files and some markdown files Floris van Doorn 2016-05-13 15:17:50 -0400
  • ac2afb6d82 doc(depgraph): update installation instructions Floris van Doorn 2016-05-13 14:49:55 -0400
  • dd5dcb1dd1 feat(hott): prove something without using ua and update book.md Floris van Doorn 2016-04-25 20:11:34 -0400
  • e9a6a532ab fixup! also allow shadowing non-constructor definitions Sebastian Ullrich 2016-06-14 00:23:21 -0400
  • d7789fa58a feat(frontends/lean): support variables shadowing in patterns Sebastian Ullrich 2016-05-29 12:20:18 -0400
  • 87c5ba9f52 Revert "fix(library/definitional/equations): add more equation validation to avoid obscure error message" Sebastian Ullrich 2016-05-16 11:40:36 -0400
  • 54844e2325 feat(frontends/lean): add parent classes to local context in struct definitions Sebastian Ullrich 2016-07-05 14:52:00 -0700
  • 3941cc1839 feat(emacs/lean-input.el): add exclude-list to lean-input-export-translations Soonho Kong 2016-06-04 05:43:38 -0400
  • d2b9fd073f feat(CMakeLists.txt): include cpp14_lang/sized_deallocation.cmake Soonho Kong 2016-06-03 12:00:43 -0400
  • c73b2860d5 fix(frontends/lean): uniform handling of declaration compound names Sebastian Ullrich 2016-05-10 18:21:31 -0400
  • bf9f3ddb3c fix(CMakeLists.txt): update cmake minimum version to 2.8.12 Soonho Kong 2016-06-02 15:38:23 -0400
  • 08b18804fd dev(lp): fix column_info initialization in lp_solver Lev Nachmanson 2016-05-20 17:46:28 -0700
  • 3d818f62a4 dev(lp): refactor the lar_core_solver parameters into a separate struct Lev Nachmanson 2016-05-20 17:07:01 -0700
  • 1529eb1e41 dev(lp): move some dummy field from lar_solver to lar_core_solver Lev Nachmanson 2016-05-20 14:30:32 -0700
  • 0bb21914e6 dev(lp): simplify the design of lar_solver Lev Nachmanson 2016-05-19 14:59:32 -0700
  • 1d3c46e712 dev(lp): add a file Lev Nachmanson 2016-05-09 15:33:52 -0700
  • d823349d2e dev(lp): integrate with z3 Lev Nachmanson 2016-05-09 15:24:47 -0700
  • b58eac5013 chore(tests/lean/extra): fix test Leonardo de Moura 2016-06-02 11:26:53 -0700
  • 273753f3fc chore(tests): mass-update for pp.binder_types false Sebastian Ullrich 2016-05-31 22:14:42 -0400
  • f2200fab65 feat(frontends/lean/pp): add option to hide binder types Sebastian Ullrich 2016-05-24 11:42:06 -0400
  • e44f9a0e62 feat(util/memory.cpp): use COMP_HAS_SIZED_DEALLOCATION macro Soonho Kong 2016-05-24 12:16:53 -0400
  • 5cda399125 feat(CMakeLists.txt): use compatibility module to check sized_deallocation feacture Soonho Kong 2016-05-24 12:15:57 -0400
  • cfc5a20b4a fix(util/memory): add C++14 sized delete operators Sebastian Ullrich 2016-05-24 08:57:34 -0400
  • 371638a628 fix(theories/analysis): rename derivative theorems Rob Lewis 2016-05-25 17:57:33 -0400
  • 6b71b75d6f fix(theories/move): add missing theorem to move Rob Lewis 2016-05-25 15:45:12 -0400
  • 5a439942dd feat(library/theories): adapt analysis theory to use new topological limits Rob Lewis 2016-05-25 15:32:24 -0400