Commit graph

6703 commits

Author SHA1 Message Date
Floris van Doorn
57514244b1 feat(hott/algebra/precategory): add todo-file for adjoint functors, equivalences and isomorphisms 2015-03-16 17:15:51 -07:00
Floris van Doorn
c914b79341 feat(hott/algebra/category): show that functor category is univalent if codomain is 2015-03-16 17:15:51 -07:00
Floris van Doorn
ebba33057c feat(hott): add arity.hlean, about multivariate functions 2015-03-16 17:15:51 -07:00
Floris van Doorn
71f9a5d1d2 feat(hott/algebra/precategory): do lots of stuff with categories 2015-03-16 17:15:51 -07:00
Leonardo de Moura
b5acbb2228 fix(frontends/lean/pp): missing parenthesis around abbreviations
fixes #476
2015-03-16 17:12:03 -07:00
Leonardo de Moura
9b577a7b3e feat(frontends/lean): add 'migrate' command 2015-03-14 21:48:00 -07:00
Leonardo de Moura
ba913876e0 feat(library/data/list/basic): enforce name conventions, add foldl_eq_foldr theorem 2015-03-14 13:06:09 -07:00
Leonardo de Moura
fc3a7bac59 feat(frontends/lean): improve error handling inside match-with expressions 2015-03-13 23:25:46 -07:00
Leonardo de Moura
bed0d6df6b fix(frontends/lean/elaborator): inaccessible over coercion 2015-03-13 23:04:45 -07:00
Leonardo de Moura
27e58dc534 refactor(library/data): cleanup vector and list modules 2015-03-13 22:25:21 -07:00
Leonardo de Moura
f6f2c499ae fix(library/tactic/rewrite_tactic): rewrite macros did not implement operator==
This problem was affecting the cache
2015-03-13 19:24:09 -07:00
Leonardo de Moura
cfeb426cd7 fix(frontends/lean): pretty print numeral notation from algebra 2015-03-13 18:58:34 -07:00
Jakob von Raumer
7083f2fccd fix(hott/algebra) correct the name of a groupoid constructor 2015-03-13 15:45:46 -07:00
Jakob von Raumer
25abecaa26 chore(hott/algebra) cmall changes in category files 2015-03-13 15:45:02 -07:00
Leonardo de Moura
362a0ec04c test(tests/lean): tests for error handling improvements 2015-03-13 15:32:25 -07:00
Leonardo de Moura
9438366e37 feat(frontends/lean/builtin_exprs): better error synchronization for 'begin...end' blocks 2015-03-13 15:22:57 -07:00
Leonardo de Moura
aba158dbd4 feat(library/tactic/inversion_tactic): improve error message for unknown hypothesis 2015-03-13 15:19:19 -07:00
Leonardo de Moura
b88b98ac22 feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
The idea is to avoid a "tsunami" of error messages when a heavily used
theorem breaks in the beginning of the file
2015-03-13 14:47:21 -07:00
Leonardo de Moura
f5811d6092 feat(frontends/lean): hide subterms that do not contain metavariables
when generating "unresolved metavariables" error message

closes #473
2015-03-13 12:42:57 -07:00
Jeremy Avigad
ec05e83a2a feat(library/data/int/div.lean): add theorems about div 2015-03-12 20:54:49 -07:00
Leonardo de Moura
a24f8dce67 refactor(hott/algebra/precategory): minor cleanup 2015-03-12 20:52:00 -07:00
Leonardo de Moura
cda19f5aa6 feat(library/tactic/rewrite_tactic): improve rewrite tactic error messages
closes #471
2015-03-12 20:49:53 -07:00
Leonardo de Moura
14aeac180a refactor(library/algebra/category/constructions): more rewrite tactic tests 2015-03-12 20:27:11 -07:00
Leonardo de Moura
adae95cf68 refactor(hott/algebra/precategory/functor): remove unnecessary annotations 2015-03-12 20:13:40 -07:00
Leonardo de Moura
265316a9f5 refactor(hott/algebra/precategory/basic): remove unnecessary set_option commands 2015-03-12 20:10:47 -07:00
Leonardo de Moura
0118ecf3cd refactor(hott/algebra/precategory/yoneda): remove unnecessary annotations 2015-03-12 20:06:25 -07:00
Leonardo de Moura
7accd0f1e6 feat(library/tactic/rewrite_tactic): allow rewrite with terms that contains binders
see discussion at #470
2015-03-12 18:07:55 -07:00
Leonardo de Moura
d7c6028a3e refactor(hott,library): use/test the rewrite tactic in more places
The performance also improved.
2015-03-12 17:25:31 -07:00
Leonardo de Moura
55586dcb2d refactor(hott/algebra/precategory/yoneda): reduce compilation time to 1sec using rewrite tactic
After the latest improvements, the rewrite tactic "works" more often
at yoneda.hlean
2015-03-12 17:07:27 -07:00
Leonardo de Moura
7ca882d69a fix(frontends/lean/parse_rewrite_tactic): esimp error message position information 2015-03-12 17:05:41 -07:00
Leonardo de Moura
026622a790 refactor(src/kernel/replace_fn): remove stack-less replace_fn it is slower than the simple one 2015-03-12 16:22:49 -07:00
Leonardo de Moura
9fe2d5c74c refactor(library/unifier): use new assign method in the unifier 2015-03-12 15:01:40 -07:00
Leonardo de Moura
4ea323a2b2 refactor(library/tactic): cleanup common pattern 2015-03-12 14:52:41 -07:00
Leonardo de Moura
8f004671a2 fix(library/unifier): typo 2015-03-12 13:15:23 -07:00
Leonardo de Moura
3e4d849a4a refactor(kernel/metavar.h): simplify API 2015-03-12 12:50:53 -07:00
Leonardo de Moura
6a78ae7b46 fix(library/tactic/class_instance_synth): enforce consistent behavior in type class resolution
Auxiliary procedure mk_class_instance was not discarding partial solutions.
This procedure is used by the apply and inversion (aka cases) tactics
2015-03-12 10:27:05 -07:00
Leonardo de Moura
b38c943086 fix(library/tactic/class_instance_synth): discard partial solutions even when option class.unique_instances = true is used 2015-03-12 10:13:16 -07:00
Leonardo de Moura
47a350d888 fix(library/tactic/inversion_tactic): missing condition for applying optimization 2015-03-12 09:11:36 -07:00
Leonardo de Moura
7de3d5771d feat(library/tactic/rewrite_tactic): add eta-reduction support at esimp
closes #469
2015-03-12 00:32:31 -07:00
Leonardo de Moura
a9fa0fead9 feat(library/match): match modulo eta 2015-03-12 00:30:44 -07:00
Leonardo de Moura
a7af8e7c71 feat(library/tactic/inversion_tactic): remove dummy hypotheses of the form (H : a = a)
closes #468
2015-03-11 20:50:06 -07:00
Leonardo de Moura
b5fb7c734e feat(library/tactic/inversion_tactic): remove hypothesis being destructed
addresses second issue in #468
2015-03-11 20:42:50 -07:00
Leonardo de Moura
0a5340aa22 feat(library/tactic/goal): add auxiliary method 2015-03-11 20:39:41 -07:00
Leonardo de Moura
ebdda67812 fix(library/tactic/inversion_tactic.cpp): remove unnecessary hypothesis in HoTT mode
partial solution for #468
2015-03-11 19:30:34 -07:00
Leonardo de Moura
737faecc65 feat(library/tactic/inversion_tactic): fail if is_hset type class synthesis produced term containing meta-variables, improve error messages
fixes #467
2015-03-11 15:54:50 -07:00
Leonardo de Moura
71ce207080 fix(frontends/lean/elaborator): potential memory access violation
Before this commit, the modified method would crash if caching in the
whnf procedure was disabled.
2015-03-11 15:54:50 -07:00
Leonardo de Moura
1c55e2f389 fix(util/memory): memory allocation problem when using clang++ 3.5 on Ubuntu 14.04 2015-03-11 10:06:13 -07:00
Leonardo de Moura
4c6b0dc0e5 fix(library/tactic/expr_to_tactic): tactic_expr_to_id did not take as_atomic annotation into account
fixes #466
2015-03-11 08:49:59 -07:00
Leonardo de Moura
1244f01518 chore(library/unifier): remove dead code 2015-03-09 14:07:14 -07:00
Leonardo de Moura
9a6c675908 feat(library/unifier): add option to disable nonchronological backtracking 2015-03-09 12:08:58 -07:00