Leonardo de Moura
94be486ade
fix(frontends/lean/builtin_cmds): generate error if declaration is not a definition
2016-05-07 18:39:40 -07:00
Leonardo de Moura
a322f5fe60
feat(compiler): start erase_irrelevant
2016-05-07 15:27:24 -07:00
Leonardo de Moura
bf5e443418
feat(frontends/lean): add #compile command back
2016-04-28 15:59:38 -07:00
Leonardo de Moura
54f68226f4
chore(frontends/lean): disable old tactic framework and blast
2016-04-25 16:22:15 -07:00
Leonardo de Moura
d88098f38d
chore(frontends/lean): remove some of the tactic support
2016-04-25 15:26:56 -07:00
Leonardo de Moura
d66406a1f4
feat(frontends/lean): add #elab command for testing new elaborator
2016-04-05 17:03:23 -07:00
Leonardo de Moura
e806700648
fix(frontends/lean/builtin_cmds): redeclare_aliases
2016-03-30 16:30:18 -07:00
Leonardo de Moura
06ef0ad7be
refactor(frontends/lean): add local_level_decls
...
Remark: the template local_decls will be deleted in the future.
The instances local_expr_decls will be replace by local_context.
2016-03-30 15:47:32 -07:00
Leonardo de Moura
3d238ee943
feat(frontends/lean/builtin_cmds): implement #unify using new type_context
2016-03-25 15:38:13 -07:00
Leonardo de Moura
487a1e7f89
refactor(kernel): remove extension_context
...
We replaced it with abstract_type_context
2016-03-19 15:15:39 -07:00
Leonardo de Moura
d8079aa16a
refactor(library): create copy of the kernel type_checker in library
...
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
2016-03-18 14:34:10 -07: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
22f3efc5be
remove(frontends/lean): begin_end pre-tactics
...
This was never used
2016-03-03 10:02:09 -08:00
Daniel Selsam
c23528b5d8
feat(library/blast/blast): use defeq_simplifier to normalize
2016-03-01 13:44:33 -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
Daniel Selsam
d521063dfb
feat(library/defeq_simplifier): new simplifier that uses only definitional equalities
2016-02-22 11:01:36 -08:00
Daniel Selsam
bb4b8da582
feat(library/unification_hint): basic handling of user-supplied unification hints
2016-02-12 11:48:51 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
22a6b7f1c3
feat(library/blast/congruence_closure): add blast.cc.heq option
2016-01-10 00:15:52 -08:00
Leonardo de Moura
42cdda227a
feat(library/congr_lemma_manager): add heterogeneous equality congruence lemmas
2016-01-09 15:41:08 -08:00
Leonardo de Moura
3ca785b0e7
refactor(library/fun_info_manager): remove dead code
2016-01-06 17:29:02 -08:00
Leonardo de Moura
1fc7bbceb2
chore(frontends/lean/builtin_cmds): handle FixedNoParam in the front-end
2016-01-03 15:18:26 -08:00
Leonardo de Moura
4eb2690c32
feat(library/scoped_ext): store set of opened namespaces
2016-01-02 13:35:08 -08:00
Leonardo de Moura
155df48665
feat(library): remove decl_stats
...
We are not using (and will not use) this module in the blast proof procedures
2016-01-02 13:00:43 -08:00
Leonardo de Moura
b117a10f82
refactor(library/blast/simplifier): use priority_queue to store simp/congr lemmas, use name convention used at forward/backward lemmas, normalize lemmas when blast starts, cache get_simp_lemmas
2015-12-28 17:52:57 -08:00
Leonardo de Moura
f177082c3b
refactor(*): normalize metaclass names
...
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).
Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write
definition foo [coercion] ...
definition bla [forward] ...
and
open [coercion] nat
open [forward] nat
It is easier to remember and is uniform.
2015-12-28 10:39:15 -08:00
Leonardo de Moura
96bec8b4f9
fix(frontends/lean/builtin_cmds): allow token and metaclass to have the same name
2015-12-28 09:57:45 -08:00
Leonardo de Moura
f679ce0da9
refactor(frontends/lean): move 'print_cmd' to separate module
2015-12-28 09:08:18 -08:00
Leonardo de Moura
d81b2d0f29
feat(library/attribute_manager, frontends/lean/builtin_cmds): use attribute manager information when pretty print definitions
2015-12-17 21:16:31 -08:00
Leonardo de Moura
7f1800962a
feat(frontends/lean/pp): allow user to override pp.all setting
...
see #922
2015-12-11 10:40:48 -08:00
Leonardo de Moura
0acdcd487b
feat(frontends/lean): add 'print aliases' command
2015-12-09 10:39:40 -08:00
Leonardo de Moura
34b944a71e
refactor(frontends/lean): remove broken 'migrate' command
2015-12-08 15:40:49 -08:00
Leonardo de Moura
7da64a768f
refactor(library/type_context): with the new tracing infrastructure, type_context doesn't need an io_state
2015-12-08 14:58:08 -08:00
Leonardo de Moura
50df6b5698
feat(frontends/lean): rename '[intro]' ==> '[intro!]' and '[backward]' ==> '[intro]'
2015-12-07 21:33:35 -08:00
Leonardo de Moura
295b1d21f5
feat(frontends/lean): add '[intro]' and '[elim]' annotations
2015-12-07 18:43:15 -08:00
Leonardo de Moura
c3b5ce0785
feat(frontends/lean/builtin_cmds): show metavariable arguments when pretty printing patterns
2015-12-07 12:39:51 -08:00
Daniel Selsam
a9aeb69789
feat(frontends/lean/builtin_cmds): print metas for patterns
2015-12-07 12:32:22 -08:00
Daniel Selsam
25a3cff54e
refactor(library/abstract_expr_manager): remove fun_info_manager
2015-12-04 08:31:38 -08:00
Daniel Selsam
7854158751
fix(library/abstract_expr_manager): only squash Cast subsingletons
2015-12-04 08:31:38 -08:00
Daniel Selsam
139536896c
feat(library/light_lt_manager): light wrappers for ordered rewriting
2015-12-02 22:56:54 -08:00
Leonardo de Moura
028ef47c84
feat(frontends/lean,library/blast/forward/pattern): check whether patterns can be inferred at declaration time
2015-12-02 22:52:55 -08:00
Leonardo de Moura
f84c6a6cfa
fix(library/blast,frontends/lean): handling pattern hints after unfolding
2015-12-02 22:52:55 -08:00
Leonardo de Moura
950f356d9a
refactor(library/blast,frontends/lean): forward pattern index
2015-12-02 22:52:55 -08:00
Leonardo de Moura
4129b398da
fix(frontends/lean/builtin_cmds): private constants in the print command
2015-12-02 22:52:54 -08:00
Leonardo de Moura
e4e9c30e66
fix(frontends/lean/builtin_cmds): print patterns
2015-12-02 22:52:54 -08:00
Leonardo de Moura
41ff4bc193
feat(library/blast/forward/pattern): pattern inference and heuristic instantiation index
2015-11-25 23:45:08 -08:00
Leonardo de Moura
0ceaf0b4fe
feat(frontends/lean/builtin_cmds): display '[forward]' annotation for heuristic instantiation lemmas
2015-11-25 17:53:13 -08:00
Leonardo de Moura
67a4cd3972
feat(frontends/lean): add print [no_pattern] command
2015-11-24 18:48:22 -08:00
Leonardo de Moura
a2f43212d6
feat(frontends/lean): add '[no_pattern]' attribute
2015-11-24 18:48:22 -08:00
