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
c0556df2ec
feat(shell/server): add "hole" server command skeleton
2017-06-14 11:44:32 -07:00
Leonardo de Moura
55c8627f2c
feat(frontends/lean): {! ... !} takes a list of pre-terms
2017-06-13 22:19:17 -07:00
Leonardo de Moura
dac6eec556
feat(library/tactic): add hole_command bookkeeping
2017-06-13 21:12:29 -07:00
Leonardo de Moura
bb2c39b471
feat(frontends/lean): add hole notation {! ... !}
...
Holes {! ... !} are elaborated using `sorry`.
We report an error if their value is fixed by typing and/or
elaboration rules.
We store the tactic_state and the optional attribute in the
info_manager. The idea is to allow users to execute commands with
respect to the stored tactic state and optional attribute.
The optional attribute is a pre term.
We are planning to add commands such as:
- Check type of the given argument.
- Reduce the given argument.
- Synthesize the hole automatically, where the given argument encodes
hint to the synthesizer.
- Use the given argument to fill the hole.
2017-06-13 18:53:05 -07:00
Johannes Hölzl
89136339ff
fix(library/init/meta): error message mentions now solve1 instead of focus
2017-06-12 20:42:48 -07:00
Johannes Hölzl
8d438e1012
feat(library/init/meta): add coinduction method
2017-06-12 20:42:48 -07:00
Johannes Hölzl
4368e6b774
fix(library/init/meta): proofs for coinductive predicates introduce now local variable
2017-06-12 20:42:48 -07:00
Johannes Hölzl
b46532bd39
feat(library/init/meta): add error messages when constructing coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
652cbee425
feat(library/init/meta): support nesting for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
3e6c7efd48
feat(library/init/meta): corec_on for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
e4d8efc91b
feat(library/init/meta): add attributes and mark parameters and locals as implicit in theorems proveded for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
f19e1742dd
feat(library/init/meta): produce cases_on for coinductive predicates
2017-06-12 20:42:48 -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
4d01a6548e
feat(library/init/meta): support mutual coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
23f12a22a2
feat(library/init/meta): add command to construct coinductive predicates
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
Armaël Guéneau
f24932748e
fix(init/meta/interactive): allow dsimp to simplify several hypothesis
2017-06-12 20:37:56 -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
Sebastian Ullrich
4c5b4fa2f4
chore(.github/PULL_REQUEST_TEMPLATE): typo
2017-06-12 09:56:15 -07:00
Jared Roesch
f3b9db99cf
chore(.github): fix typo
2017-06-12 09:56:15 -07:00
Jared Roesch
47df98aaf0
chore(., .github): move templates to .github
2017-06-12 09:56:15 -07:00
Jared Roesch
5ff6f40897
feat(.): add first pass at contributing & issue & pr templates
2017-06-12 09:56:15 -07:00
Gabriel Ebner
3c0420230f
fix(leanpkg): typo
2017-06-12 17:54:46 +02:00
Gabriel Ebner
ee4b9bd5c5
fix(leanpkg): run configure after upgrade
2017-06-12 17:48:14 +02:00
Gabriel Ebner
a5677d6456
feat(leanpkg): upgrade command
2017-06-12 17:46:11 +02:00
Gabriel Ebner
dc81915da6
refactor(library): unify char.to_string and char.has_to_string
2017-06-12 16:32:35 +02:00
Gabriel Ebner
0e864e5e9f
chore(doc/bin/README): remove options that no longer exist
2017-06-12 15:42:40 +02:00
Gabriel Ebner
fa8d690559
feat(extras/depgraph): add dependency-free version of leandeps
2017-06-12 15:40:46 +02:00
Gabriel Ebner
ee8b2b39fe
chore(library): remove gdb_history file
2017-06-12 15:39:46 +02:00
Gabriel Ebner
bca62c1368
chore(*): remove obsolete .project files
2017-06-12 15:38:17 +02:00
Gabriel Ebner
1a81425098
chore(library): convert comments to docstrings
2017-06-12 15:17:00 +02:00
Sebastian Ullrich
8849df0d3e
chore(script/test_registry): don't stop on failure
2017-06-09 20:30:48 +02:00
Daniel Selsam
8f875c92ba
fix(inductive_compiler/nested.cpp): fixes #1657
2017-06-09 20:06:50 +02:00
Jeremy Avigad
8de8870124
fix(leanpkg/leanpkg/toml.lean): use correct to_string method for char
2017-06-09 17:18:35 +02:00
Sebastian Ullrich
fd8c1de428
fix(emacs/lean-type): replace non-stable function
2017-06-08 22:58:51 +02:00
Sebastian Ullrich
1bab73e10c
fix(init/meta/interactive_base): fix sformat! macro
2017-06-08 16:22:50 +02:00
Rob Lewis
6f545718a0
fix(reflect): move format instance to expr.lean
2017-06-08 15:54:41 +02:00
Rob Lewis
b8e5de2fb7
fix(reflect): change names
2017-06-08 15:54:41 +02:00
Rob Lewis
0e0070eb2f
feat(reflect): add formatting instances and make nat.reflect 0 a numeral
2017-06-08 15:54:41 +02:00
Sebastian Ullrich
85905ccbb8
fix(emacs/lean-type): do not update *Lean Goal* buffer if new state is empty
2017-06-08 11:31:01 +02:00
Sebastian Ullrich
587cf6c050
fix(emacs/lean-mode): update *Lean Goal* buffer on flycheck changes
2017-06-08 11:29:19 +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
Mario Carneiro
26a377753a
fix(init/meta/interactive): let case tactic support _ names
2017-06-07 18:09:15 -07:00
Leonardo de Moura
0b04376676
refactor(library/init/data/string/basic): mark string implementation as private
...
See issue #1175
BTW, we may have to revise this decision in the future when we decide to
populate the string library with lemmas.
It is inconvenient to prove the lemmas at string/basic.lean since the
tactic framework has not been defined yet.
Anyway, I think it is worth to keep the private for now, and make sure
nobody relies on its implementation.
2017-06-07 18:00:24 -07:00
