Leonardo de Moura
cfa34dc83e
chore(library): remove workarounds for issue #1682
2017-06-19 16:09:12 -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
4d444b8b18
feat(init/meta/lean/parser): persist environment in tactic_to_parser
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
Gabriel Ebner
2e142d87ae
fix(library/init/data/repr): give correct implementation of nat.repr
2017-06-19 16:20:27 +02:00
Gabriel Ebner
82bb37422d
fix(library/init/data/int): add to_string instance for integers
2017-06-19 14:30:58 +02: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
049fecee23
fix(library/init): name has_repr instance is actually a has_to_string instance
...
See #1664
2017-06-18 18:33:16 -07:00
Leonardo de Moura
8b88f21c91
refactor(library): add has_to_string back (but it produces unquoted values)
...
See issue #1664
2017-06-18 18:30:10 -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
Leonardo de Moura
7528e14e68
feat(frontends/lean,shell/server): "hole" command
2017-06-14 21:56:17 -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
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
Gabriel Ebner
dc81915da6
refactor(library): unify char.to_string and char.has_to_string
2017-06-12 16:32:35 +02:00
Gabriel Ebner
ee8b2b39fe
chore(library): remove gdb_history file
2017-06-12 15:39:46 +02:00
Gabriel Ebner
1a81425098
chore(library): convert comments to docstrings
2017-06-12 15:17:00 +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
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
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
Leonardo de Moura
84260544d5
feat(library/init/meta/well_founded_tactics): improve trivial_nat_lt
2017-06-07 15:47:56 -07:00
Mario Carneiro
c13472a8b8
feat(init/meta/interactive): change-with tactic
...
Conflicts:
library/init/meta/interactive.lean
2017-06-07 10:33:14 -07:00
Mario Carneiro
e8e57dcb15
feat(init/meta/interactive): change at tactic
...
addresses #1641
2017-06-07 10:17:00 -07:00
Sebastian Ullrich
3f717c586e
feat(init/meta/interactive): declare format! and sformat! macros and start putting them to use
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
38aa99e7a5
fix(init/meta/has_reflect): reflect 1
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
79f29a693e
refactor(init/meta/interactive): split file
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
59184e888f
feat(init/meta/pexpr): has_to_pexpr (reflected a)
2017-06-07 10:09:38 -07:00
Mario Carneiro
77264a6074
fix(init/meta/interactive): get rhs using relation_lhs_rhs
2017-06-07 10:03:35 -07:00
Mario Carneiro
1354514c80
feat(init/meta/interactive): specify intermediate goal in transitivity
...
As suggested by @Armael on gitter
2017-06-07 10:03:23 -07:00
Leonardo de Moura
9b60e25ca4
fix(library/init/meta/level): make level as meta
2017-06-06 16:12:35 -07:00
Leonardo de Moura
3bc414efff
perf(library/tactic): add unsafe_change tactic
...
The `unsafe_change e` tactic is similar to the `change e` tactic, but it
does not check whether `e` is definitionally equal to the current
tactic. It is useful when implementing tactics such as:
```
meta def dunfold : list name → tactic unit :=
λ cs, target >>= dunfold_core transparency.instances default_max_steps cs >>= unsafe_change
```
The tactic `dunfold_core` guarantees that the resultant expression is
definitionally equal to the input one.
This was one of the performance problems at issue #1646 .
Here are the runtimes for size 7 in the example described at issue #1646 .
Before this commit:
tactic execution took 4.96s
elaboration of some_lifted_lets took 7.6s
type checking time of some_lifted_lets took 31.1ms (aka QED time)
total execution time: 12.785s
After this commit:
tactic execution took 3.78s
elaboration of some_lifted_lets took 5.71s
type checking time of some_lifted_lets took 35.2ms
total execution time: 10.693s
2017-06-06 14:55:25 -07:00
