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

Commit graph

  • 2c56a2c48b feat(theories/{analysis, topology}): show eps-delta and topological continuity coincide on metric spaces Rob Lewis 2016-02-09 16:36:14 -0500
  • eb05741ce6 feat(data/set): add missing set membership theorems Rob Lewis 2016-02-09 16:35:40 -0500
  • 685049988c feat(theories/analysis): define metric topology Rob Lewis 2016-02-08 13:57:10 -0500
  • b8d86ffe48 feat(theories/topology): add theorem for proving sets open Rob Lewis 2016-02-08 12:07:51 -0500
  • bb4b8da582 feat(library/unification_hint): basic handling of user-supplied unification hints Daniel Selsam 2016-02-12 09:03:06 -0800
  • d8fb6f5082 fix(bin/linja.in): wrap args.cache to avoid problems handling fullpath with space Soonho Kong 2016-02-11 16:40:21 -0500
  • 632d4fae36 chore(library): rename local_context to old_local_context Leonardo de Moura 2016-02-11 11:59:11 -0800
  • 74192b0cb8 chore(library): remove dead code Leonardo de Moura 2016-02-11 18:08:44 -0800
  • c9e9fee76a refactor(*): remove name_generator and use simpler mk_fresh_name Leonardo de Moura 2016-02-10 17:17:22 -0800
  • 9cbda49297 chore(frontends/lean): remove script blocks Leonardo de Moura 2016-02-08 18:50:00 -0800
  • f67181baf3 chore(*): remove support for Lua Leonardo de Moura 2016-02-08 18:42:34 -0800
  • 3de4ec1a6c fix(library/blast/imp_extension): do not use the name 'assert' Daniel Selsam 2016-02-10 14:10:03 -0800
  • 42b78962f9 feat(init/wf): simplify definition acc.drec Floris van Doorn 2016-02-08 20:15:57 -0500
  • e14d4a4c0c feat(init/wf): port from standard library to HoTT library Floris van Doorn 2016-02-08 20:07:44 -0500
  • c0abcc7722 chore(hott): fix signature of previous lemma Jakob von Raumer 2016-02-09 13:21:38 +0000
  • 3c7536cff8 chore(hott): clean up cancellability proof a bit Jakob von Raumer 2016-02-09 13:12:30 +0000
  • 4d6c516c01 feat(hott): add lemma: equivalent fin sets come from equal numbers, sums with fin sets are cancellable Jakob von Raumer 2016-02-08 17:20:19 +0000
  • 4edb6d7765 feat(hott): finish cancelling law for sums with unit Jakob von Raumer 2016-02-08 16:19:20 +0000
  • 0ad8131985 feat(hott): start cancellation proof for sums Jakob von Raumer 2016-02-08 11:44:10 +0000
  • 62e1431f04 chore(hott): delay lemmas about smash product until I have more ideas on how to tackle the coherence there. Jakob von Raumer 2016-02-02 18:45:52 +0000
  • 1042f6c29d feat(hott): port finite ordinal sets from the std library, with all things related to nat.mod and to fintype still missing. Jakob von Raumer 2016-02-02 18:44:01 +0000
  • cb3bc1a311 feat(hott): add another constructor for pointed equivalences Jakob von Raumer 2016-01-29 15:07:39 +0000
  • 23dec19aa7 feat(hott): start lemma about smashing with bool Jakob von Raumer 2016-01-27 17:12:57 +0000
  • 8bc4206c62 feat(hott): add custom recursors for cofiber type Jakob von Raumer 2016-01-27 14:59:54 +0000
  • 31e2653e58 feat(hott): add lemma: cofiber of terminal morphism is suspension Jakob von Raumer 2016-01-27 11:48:32 +0000
  • 7e02ea6cab feat(hott): add smash product of pointed types Jakob von Raumer 2016-01-26 17:14:45 +0000
  • ce8ca64771 feat(hott): adjust small things in wedge theory Jakob von Raumer 2016-01-25 16:54:48 +0000
  • 56cd88267c feat(hott): add cofiber of a function, prove lemma that cofibers of equivalences are contractible Jakob von Raumer 2016-01-25 16:54:24 +0000
  • f06cdff2a1 fix(library/blast/simplifier/ceqv): fix error in is_permutation Daniel Selsam 2016-02-04 17:20:03 -0800
  • ec38ee8df8 fix(hott/init/tactic): add replace Floris van Doorn 2016-02-04 22:30:39 -0500
  • 668758c44e fix(library/blast/blast): compilation warning on OSX Leonardo de Moura 2016-02-05 13:02:02 -0800
  • 6c1c6cbbdd fix(util/lp,tests/util/lp): warning msgs on OSX Leonardo de Moura 2016-02-05 10:46:29 -0800
  • e785827688 fix(tests/util/lp/CMakeFiles): disable lp test that fails when executing ctest Leonardo de Moura 2016-02-05 10:12:11 -0800
  • 1c8d8da9cf chore(util/lp/lp_primal_core_solver): fix warning Leonardo de Moura 2016-02-05 10:07:54 -0800
  • 0e4f98dc47 dev(lp): remove a warning Lev Nachmanson 2016-02-03 16:48:19 -0800
  • a7e3befd21 dev(lp): speed up primal with sorted list Lev Nachmanson 2016-02-03 16:45:51 -0800
  • ff8213a6a9 dev(lp): diminish the number of pivots of primal by sorting the columns Lev Nachmanson 2016-02-02 13:00:45 -0800
  • 61eaef0183 dev(lp): improve the dual perormance Lev Nachmanson 2016-02-02 09:35:04 -0800
  • 9482d508df dev(lp): fix bugs in the dual simplex high loop Lev Nachmanson 2016-02-01 15:53:01 -0800
  • fbe4f56aea chore(lp): remove warnings Lev Nachmanson 2016-01-26 14:40:29 -0800
  • 739f9e5486 fix(tests/util/lp/lp): use regular C arrays Leonardo de Moura 2016-01-26 13:17:36 -0800
  • 40d4623219 fix(util/lp/lp_settings): replace fabs with std::abs Leonardo de Moura 2016-01-26 13:17:13 -0800
  • 971ec72157 fix(util/lp/numeric_pair): include cmath Leonardo de Moura 2016-01-26 13:16:52 -0800
  • 504c603af4 chore(lp): use std::ostream for printing routines Lev Nachmanson 2016-01-25 14:49:23 -0800
  • fc858d98c0 chore(lp): improve formatting Lev Nachmanson 2016-01-21 11:33:09 -0800
  • e9cd621855 chore(lp): improve formatting Lev Nachmanson 2016-01-21 11:03:55 -0800
  • 28bf891b7f dev(lp): port to windows (msys2) Lev Nachmanson 2016-01-12 03:11:23 -0800
  • 99dcad0dda dev(lp): performance tuning in find_leaving_on_harris_theta Lev Nachmanson 2016-01-11 11:07:02 -0800
  • d098dfe326 dev(lp): fix infeasibility evidence check Lev Nachmanson 2016-01-09 01:35:30 -0800
  • d9acf90f7b refactor(util/lp): use Lean exception Leonardo de Moura 2016-01-08 15:59:45 -0800
  • 8fbf66d01a chore(util/lp): no "using", indentation Leonardo de Moura 2016-01-08 15:50:24 -0800
  • 1841d17544 refactor(lp): NDEBUG ==> LEAN_DEBUG Leonardo de Moura 2016-01-08 14:34:21 -0800
  • fbb3ed8911 feat(lp): add LP solver and incremental LU factorization Lev Nachmanson 2013-10-14 10:57:55 -0700
  • 04eaf184a9 feat(frontends/lean,library/unifier): checkpoints at have-expressions Leonardo de Moura 2016-02-04 18:41:55 -0800
  • 30d6853ffd refactor(hott,tests): make sure HoTT library and tests still work if we introduce checkpoints in have-expressions Leonardo de Moura 2016-02-04 12:20:50 -0800
  • a08bc408c8 fix(frontends/lean/structure_cmd): fixes #967 Leonardo de Moura 2016-02-04 16:15:18 -0800
  • 31cc0ebb6a fix(frontends/lean/structure_cmd): fixes #968 Leonardo de Moura 2016-02-04 15:44:54 -0800
  • 496c84dac6 fix(frontends/lean/elaborator): fixes #982 Leonardo de Moura 2016-02-04 15:14:30 -0800
  • 774fa01b1a chore(library/pp_options): reduce pp default limits Leonardo de Moura 2016-02-04 14:55:21 -0800
  • f62e22b34c fix(util/sexpr/format): fixes #955 Leonardo de Moura 2016-02-04 14:45:35 -0800
  • 0268f92eb4 fix(frontends/lean/elaborator): fixes #965 Leonardo de Moura 2016-02-04 13:41:21 -0800
  • 42fbc63bb6 fix(library/tc_multigraph): avoid name collisions Leonardo de Moura 2016-02-04 13:15:42 -0800
  • dcb35008e1 feat(hott/homotopy): general connectivity elimination and the wedge connectivity lemma Ulrik Buchholtz 2016-01-23 14:15:59 -0500
  • 87ec5ada07 fix(analysis/metric_space): unnecessary import, style, remove unnecessary lines Rob Lewis 2016-02-02 13:22:21 -0500
  • a675a5ede2 fix(algebra/ordered_field, analysis/real_limit): generalize theorem to ordered fields Rob Lewis 2016-02-01 15:51:29 -0500
  • f402f322aa feat(theories/analysis): add theorems about convergent sequences, functions, and continuity Rob Lewis 2016-02-01 15:40:21 -0500
  • ffed988a34 feat(data/list): add missing theorems Rob Lewis 2016-02-01 15:39:40 -0500
  • dcfc496992 feat(algebra/ordered_field): ad missing theorem Rob Lewis 2016-02-01 15:39:08 -0500
  • 40a1371cd0 feat(theories/analysis): define real square roots Rob Lewis 2016-01-28 17:26:16 -0500
  • 796e16bdb7 feat(library/theories/analysis): add theorems about convergent functions in metric spaces Rob Lewis 2016-01-28 17:24:39 -0500
  • cb4f71b16c feat(library/data/real): add more theorems concerning rationals embedded in reals Rob Lewis 2016-01-28 17:23:02 -0500
  • 110036c4dc feat(library/algebra/ordered_field): add missing theorems Rob Lewis 2016-01-28 17:21:28 -0500
  • 790dbc53c3 refactor(library/algebra/ring): cleanup Leonardo de Moura 2016-02-03 20:07:12 -0800
  • cb12b9b876 refactor(library): cleanup proofs Leonardo de Moura 2016-02-03 19:20:29 -0800
  • 9d88db3941 perf(library/type_context): add cache for minimizing the access to is_opaque and environment::find Leonardo de Moura 2016-02-02 19:44:16 -0800
  • 701d6b5016 perf(library/blast/forward/pattern): simplify is_higher_order test Leonardo de Moura 2016-02-02 18:56:48 -0800
  • a7b3dcbc09 perf(library/blast/state): do not add hypotheses that are Pi-expressions into discrimination trees Leonardo de Moura 2016-02-02 18:46:09 -0800
  • 4324726a8e perf(kernel/expr_eq_fn): minimize number of calls to check_system Leonardo de Moura 2016-02-02 18:16:14 -0800
  • c55b10af1b perf(library/type_context): move check_system to strategic places Leonardo de Moura 2016-02-02 16:12:53 -0800
  • b508cf813c perf(library/type_context): small optimization Leonardo de Moura 2016-02-02 15:36:53 -0800
  • bc86e9f179 perf(library/type_context): add caching for type_context::infer Leonardo de Moura 2016-02-02 15:17:18 -0800
  • bd52e58294 perf(util/name): use quick_cmp at name_pair_quick_cmp Leonardo de Moura 2016-02-02 13:54:48 -0800
  • cb203c3272 perf(src/util/name): if the hashcodes are equal, then there is a high probability the names are equal Leonardo de Moura 2016-02-02 12:52:06 -0800
  • a9cb9ff912 perf(util/name): more inlining Leonardo de Moura 2016-02-02 09:49:50 -0800
  • 187bce307e perf(src/util/name): inline hash Leonardo de Moura 2016-02-02 09:21:01 -0800
  • c779590517 feat(library/algebra/ring): add lemma Leonardo de Moura 2016-01-30 16:34:59 -0800
  • a7b37d0e09 perf(library/type_context): cache type class resolution failures too Leonardo de Moura 2016-01-29 14:06:47 -0800
  • 6b137b7dd3 chore(library/blast/forward/ematch): improve comment Leonardo de Moura 2016-01-29 11:55:51 -0800
  • 587c263c28 feat(library/blast/forward/ematch): improve support for casts in the e-matcher Leonardo de Moura 2016-01-29 11:38:43 -0800
  • 6ed6306c3f fix(library/blast/unit/unit_propagate): use ppb when tracing Daniel Selsam 2016-01-27 14:39:46 -0800
  • 684995640a fix(library/blast/unit/unit_propagate): memory access violation Leonardo de Moura 2016-01-27 15:22:34 -0800
  • fb95b71a5e fix(library/blast/forward/pattern): bug in the pattern inference code Leonardo de Moura 2016-01-27 13:27:58 -0800
  • a713ca9686 feat(library/type_context): add helper method get_num_choice_points Leonardo de Moura 2016-01-26 22:02:25 -0800
  • 12e148c7b6 feat(library/blast/forward/ematch): even more tracing Daniel Selsam 2016-01-26 21:37:35 -0800
  • 30b5313118 feat(CMakeLists.txt): handle new/old ABIs issue for MSYS2 + g++ combination Soonho Kong 2016-01-18 11:56:10 -0500
  • 2868ec9c43 fix(library/blast/trace): missing pragma Daniel Selsam 2016-01-25 13:47:59 -0800
  • eca079a4fc feat(library/blast/unit/unit_propagate): basic tracing Daniel Selsam 2016-01-25 14:44:01 -0800
  • 29c84aad19 fix(book.md): add types.arrow to 2.9 Floris van Doorn 2016-01-26 12:59:01 -0500
  • 810ee9759c fix(library/blast/backward/backward_action): add missing normalize at backward_action, and remove incorrect fix at discrimination tree Leonardo de Moura 2016-01-26 20:35:57 -0800
  • 4821af8685 feat(frontends/lean/scanner): disallow superscripts in identifiers Leonardo de Moura 2016-01-26 18:24:12 -0800