Leonardo de Moura
2075ec8d61
fix(library/equations_compiler/elim_match): bad trace message
2017-06-25 10:50:40 -07:00
Gabriel Ebner
16fb5ade58
fix(library/string): correctly escape non-printable characters
...
This also fixes a compiler warning on ARM, where `0 <= c` is always
true.
2017-06-23 20:39:41 +02:00
Gabriel Ebner
4a6513e5f5
refactor(util/serializer,library/module): use basic_ostream::write for the olean code
2017-06-23 15:13:40 +02:00
Leonardo de Moura
9cb94847cb
fix(library/equations_compiler): propagate m_ignore_if_unused flag
2017-06-22 17:01:31 -07:00
Leonardo de Moura
58f0561f41
fix(library/equations_compiler/equations): is_equation
2017-06-22 17:01:08 -07:00
Leonardo de Moura
e905e83e9e
chore(library, frontends/lean): use override
2017-06-22 16:15:21 -07:00
Leonardo de Moura
096b437c11
fix(library/equations_compiler, frontends/lean): missing operator== for macro_definition_cell subclasses
2017-06-22 16:13:29 -07:00
Gabriel Ebner
30a9217a78
feat(library/type_context): unfold lemmas in major premise of acc.rec
2017-06-22 08:33:11 -07:00
Leonardo de Moura
3195a800f4
feat(library/tactic/simp_lemmas): use proof for refl lemmas at simp_lemma_rewrite too
...
I forgot to do it at 9fcb3ae4b5
2017-06-21 16:53:35 -07:00
Leonardo de Moura
b9dee04fdb
feat(library/tactic/simplify): add single_pass simplifier option (default is false)
2017-06-21 16:41:54 -07:00
Leonardo de Moura
9fcb3ae4b5
feat(library/tactic/simplify): store proof for refl lemmas and use them in simp
...
Before this commit, simp would not silently apply refl-lemmas, and use
reflexivity. This strategy produces compact proofs but may generate
performance problems. For example, the new test timeouts without this
commit.
I believe a similar performance problem is affecting the Certigrad
project developed by @dselsam.
2017-06-21 16:21:11 -07:00
Leonardo de Moura
fd17a19a23
chore(library/tactic/simplify): remove dead option
2017-06-21 15:32:08 -07:00
Gabriel Ebner
814a5edaf1
fix(library/module_mgr): check for errors when writing olean files
2017-06-21 11:25:25 +02:00
Gabriel Ebner
a0a70a678a
fix(library/module): check for end-of-file in deserialization
2017-06-21 11:25:25 +02:00
Gabriel Ebner
942f7bf8b5
fix(library/module): unify hash computation
2017-06-21 10:50:54 +02:00
Leonardo de Moura
e089fe6ee7
fix(library/expr_lt): make sure find_local_decl is not tested in the Meta case, and add /* fall-thru */
...
See comments at commit b25291c5c9
2017-06-20 13:47:30 -07:00
Leonardo de Moura
b25291c5c9
fix(library/tactic/simplify): fixes #1685
2017-06-20 12:27:46 -07:00
Leonardo de Moura
ce3387b246
fix(library/tactic/change_tactic): fixes #1686
2017-06-20 12:05:21 -07:00
Leonardo de Moura
3c306d0a7b
fix(library/equations_compiler/elim_match): forward dependency checking
...
See comment at #1594
This commit is not fixing the issue, but a problem described in one of
the comments.
2017-06-20 11:29:23 -07:00
Sebastian Ullrich
91c77680c8
refactor(init/meta/coinductive_predicates,frontends/lean/inductive_cmds): declare coinductive in Lean
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
018ebdd115
feat(frontends/lean/user_command): add user-defined commands
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
606cc85778
chore(library/module): output byte offset of olean corruption
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
492cb20438
feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env
2017-06-19 11:27:12 -07:00
Leonardo de Moura
b8fa7f5311
fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean
...
See #1664
2017-06-18 18:33:27 -07:00
Leonardo de Moura
dc1a1c8540
refactor(library): has_to_string ==> has_repr
...
See issue #1664
This is just the first step to implement proposal described at issue #1664 .
2017-06-18 18:29:19 -07:00
Daniel Selsam
cda196f278
perf(library/delayed_abstraction.cpp): stack caches when pushing delayed abstractions
2017-06-18 10:24:20 -07:00
Leonardo de Moura
bf0d785888
feat(library/messages, frontends/lean): optional end position for messages
...
We need this information to be able to fix issues with the transient
message boxes feature (#1667 ).
2017-06-15 10:47:58 -07:00
Leonardo de Moura
5cb96c7fa3
feat(frontends/lean): add option for pretty printing metavars, sorry and delayed abstractions as holes
...
This option is false by default, but true when executing hole commands
2017-06-15 10:24:26 -07:00
Gabriel Ebner
5528a26592
fix(library/tactic/tactic_state): make tactic.sleep interruptible
...
Fixes leanprover/vscode-lean#52
2017-06-15 17:16:40 +02:00
Leonardo de Moura
3700bb4568
chore(library/tactic/hole_command,frontends/lean/interactive): fix style
2017-06-14 22:23:25 -07:00
Leonardo de Moura
7557a9e000
feat(shell/server,frontends/lean): add "hole_commands" server command
...
The new command returns the list of registered/applicable hole
commands.
2017-06-14 22:16:34 -07:00
Leonardo de Moura
7528e14e68
feat(frontends/lean,shell/server): "hole" command
2017-06-14 21:56:17 -07:00
Leonardo de Moura
dac6eec556
feat(library/tactic): add hole_command bookkeeping
2017-06-13 21:12:29 -07:00
Johannes Hölzl
1352d4a5b3
feat(src/frontents/lean): support for coinduction command in frontend
2017-06-12 20:42:48 -07:00
Johannes Hölzl
e88933bac9
feat(library/init/meta/tactic): add tactic.set_env to set environment
2017-06-12 20:42:48 -07:00
Leonardo de Moura
9d5b69ad5c
fix(library/compiler/preprocess): compile_lemma => compile_irrelevant
...
We can also ignore functions that return types at compile_lemma (now
called compile_irrelevant).
fixes #1658
2017-06-12 20:33:31 -07:00
Leonardo de Moura
f5e34f0c02
chore(library): make sure replace_visitor behavior is not compiler dependent, and remove code duplication
2017-06-12 20:18:11 -07:00
Leonardo de Moura
d7e3bd794e
fix(library/equations_compiler): fixes #1663
2017-06-12 19:45:01 -07:00
Daniel Selsam
8f875c92ba
fix(inductive_compiler/nested.cpp): fixes #1657
2017-06-09 20:06:50 +02:00
Gabriel Ebner
4b05c645bb
fix(library/constructions/injective): use same transparency setting as no_confusion
2017-06-08 10:17:21 +02:00
Leonardo de Moura
17f8231d59
feat(library/tactic/cases_tactic): add support for injective functions in the cases tactic
...
This feature is needed when we declare an inductive predicate/type
which is indexed by a mutual and/or nested inductive datatype.
See tests/lean/run/term_pred.lean for an example.
@Armael: this commit should fix the issue with the `cases` tactic that
you reported today.
2017-06-07 19:50:01 -07:00
Leonardo de Moura
4eefc41b6e
refactor(*): wrap string in a structure
...
We want to make sure string users do not depend on the string
implementation. This is the first step.
We need this refactoring *now* to make sure it will not be
super painful to address issue #1175
2017-06-07 17:30:49 -07:00
Sebastian Ullrich
b60899138e
fix(library/vm/vm_parser): header worries after rebase
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
dd91630a83
feat(frontends/lean/user_notation): more error checking
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
01c430cd62
fix(frontends/lean/{parser_config,user_notation): persisting user notations
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
56995348d3
hack(frontends/lean/parser): allow input to be substituted and use it to implement interpolating format macro
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
2bb93aa4f9
feat(init/meta): tactic -> parser coercion
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
20ab8feeae
feat(init/meta/lean/parser): pexpr parser that does not use quoted mode
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
18063fa9ba
feat(frontends/lean): user-defined notation parsers
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
be6f2eada7
chore(*): typos
2017-06-07 10:09:38 -07:00
