Leonardo de Moura
fdbe8ee98a
feat(library/local_context): add get_local_decl_from_user_name
2016-03-05 13:35:54 -08:00
Leonardo de Moura
c8e5907b70
feat(util/rb_tree,util/rb_map): add back_find_if
2016-03-05 13:29:34 -08:00
Leonardo de Moura
c3568e1ebb
fix(library/local_context): typo in assertion
2016-03-05 13:28:33 -08:00
Leonardo de Moura
66d583d279
feat(library/local_context): add well_formed debugging methods
2016-03-05 13:09:36 -08:00
Leonardo de Moura
4543dc4a7f
feat(library): add metavar_context
2016-03-05 12:53:45 -08:00
Leonardo de Moura
994c9298b5
feat(library/local_context): add local_decls (set), and freeze operation for local declarations
2016-03-04 13:59:11 -08:00
Leonardo de Moura
05f58547c5
chore(library/type_context): rename type_context to old_type_context
...
We are going to implement a new type_context object.
2016-03-04 10:51:04 -08:00
Leonardo de Moura
eaac6ba721
chore(library/type_context): rename default_type_context to legacy_type_context and move it to different file
2016-03-04 10:26:50 -08:00
Leonardo de Moura
9d0dfb8404
refactor(frontends/lean): remove calc_proof_elaborator
2016-03-03 17:22:45 -08:00
Leonardo de Moura
227b548341
refactor(frontends/lean/calc): no overloading in calc steps
2016-03-03 15:00:51 -08:00
Leonardo de Moura
2c70ca83a8
refactor(frontends/lean/calc): remove '{}' notation for eq.subst in calc mode
2016-03-03 14:18:20 -08:00
Leonardo de Moura
d7de521126
refactor(library/class): remove attribute [multiple_instances] and old type class resolution procedure
2016-03-03 13:58:22 -08:00
Leonardo de Moura
4a43e33d45
chore(*): disable big chunk of the standard library and tests
2016-03-03 13:43:08 -08:00
Leonardo de Moura
f0158ba20c
chore(CMakeLists): disable HoTT library and tests
2016-03-03 12:51:10 -08:00
Floris van Doorn
e5d5ef9d55
feat(hott/library): various changes and additions.
...
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
2016-03-03 10:13:20 -08:00
Leonardo de Moura
d84a20d68b
remove(frontends/lean/server): FINDG command
2016-03-03 10:12:24 -08:00
Leonardo de Moura
22f3efc5be
remove(frontends/lean): begin_end pre-tactics
...
This was never used
2016-03-03 10:02:09 -08:00
Leonardo de Moura
d54a67cf2e
fix(library): compilation warnings on OSX
2016-03-03 10:02:00 -08:00
Leonardo de Moura
6f766dd33e
chore(library/blast): cleanup
2016-03-03 10:01:50 -08:00
Leonardo de Moura
5194df5e97
feat(library/local_context): encode order using a tree instead of a list
...
Motivations:
- It will be faster to delete local declarations.
- It is faster to find all local declarations that were created after a
give local declaration.
2016-03-01 16:23:51 -08:00
Leonardo de Moura
82fb38b440
feat(util/rb_tree): add for_each_greater
2016-03-01 15:42:27 -08:00
Leonardo de Moura
2a4b3b75bd
refactor(library/blast/state): simplify blast state
2016-03-01 14:27:58 -08:00
Leonardo de Moura
16dc021736
fix(library/proof_irrel_expr_manager): add missing Let case
2016-03-01 14:27:37 -08:00
Leonardo de Moura
4e67a35179
feat(library/blast/blast): add missing Let case, and comment to indicate
...
performance problem
2016-03-01 13:47:43 -08:00
Daniel Selsam
c23528b5d8
feat(library/blast/blast): use defeq_simplifier to normalize
2016-03-01 13:44:33 -08:00
Daniel Selsam
20e7ff39cc
feat(library/proof_irrel_expr_manager): eq and hash modulo proof irrelevance
2016-03-01 13:44:33 -08:00
Daniel Selsam
a9c6bce7cc
feat(library/defeq_simplifier): some generic normalization
2016-03-01 13:43:50 -08:00
Leonardo de Moura
2982db6f80
feat(library/local_context): add new local context type
2016-03-01 13:40:37 -08:00
Leonardo de Moura
f3648e2ac8
refactor(library/blast/blast): remove old hack
2016-03-01 12:24:24 -08:00
Leonardo de Moura
56d7fc4c23
refactor(*): cleanup replace_visitor subclasses, and make sure let-expressions are handled
2016-02-29 16:55:19 -08:00
Leonardo de Moura
3c878ecd01
feat(kernel): add let-expressions to the kernel
...
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
2016-02-29 16:40:17 -08:00
Leonardo de Moura
f55e456c84
chore(*): remove remaining references to by+ and begin+
2016-02-29 13:59:06 -08:00
Leonardo de Moura
b7b4b6d838
chore(src/frontends/lean/builtin_exprs): remove unnecessary parameter
2016-02-29 13:57:18 -08:00
Leonardo de Moura
f54963bc3e
refactor(library/tactic/expr_to_tactic): remove 'by_plus' support
2016-02-29 13:50:05 -08:00
Leonardo de Moura
fbe5188480
refactor(frontends/lean): remove 'by+' and 'begin+' tokens
2016-02-29 13:45:43 -08:00
Leonardo de Moura
bf60999ede
fix(frontends/lean/builtin_exprs): 'using' expression
2016-02-29 13:23:39 -08:00
Leonardo de Moura
15c4bc92b9
refactor(frontends/lean/elaborator): we only need to track one context
2016-02-29 12:49:17 -08:00
Leonardo de Moura
2b1d734544
feat(kernel/expr): remove 'contextual' flag from binder_info
2016-02-29 12:41:43 -08:00
Leonardo de Moura
b41c65f549
feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking
2016-02-29 12:31:23 -08:00
Leonardo de Moura
101cf1ec4c
feat(frontends/lean): remove difference between 'have' and 'assert'
2016-02-29 11:28:20 -08:00
Lev Nachmanson
23079a75a7
dev(lp): fix build for clang, avoid clang-3.3 bug, cleanup permutation_matrix
...
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-26 16:07:16 -08:00
Leonardo de Moura
2fd5347901
refactor(library/blast): ppb is not necessary anymore
2016-02-26 15:51:46 -08:00
Leonardo de Moura
eee74ef1b4
refactor(frontends/lean/pp): use abstract_type_context instead of type_checker
2016-02-26 15:35:29 -08:00
Leonardo de Moura
7d61f640f6
refactor(*): add abstract_type_context class
2016-02-26 14:17:34 -08:00
Leonardo de Moura
5a4dd3f237
feat(library/reducible): remove [quasireducible] annotation
2016-02-25 17:42:44 -08:00
Leonardo de Moura
146edde5b3
feat(library/class): mark instances as quasireducible by default
...
quasireducible are also known as lazyreducible.
There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.
2016-02-25 12:11:29 -08:00
Leonardo de Moura
1924b2884c
refactor(library/tactic): remove 'append' and 'interleave' tacticals
...
Preparation for major refactoring in the tactic framework.
2016-02-24 16:02:16 -08:00
Leonardo de Moura
9b15c4c669
feat(util/rb_map): add find_if
2016-02-24 16:02:16 -08:00
Leonardo de Moura
494b88e103
fix(library/blast/forward/ematch): must used the right type_context
2016-02-23 13:32:34 -08:00
Sebastian Ullrich
2a35c0f49b
feat(script): add .md link checker script
2016-02-23 10:11:24 -08:00
