Leonardo de Moura
a1dc121eee
feat(library/init/meta/environment): add environment.fingerprint API
2017-06-02 16:52:40 -07:00
Leonardo de Moura
c59543bde8
feat(library/init/meta/tactic): add sleep tactic for debugging purposes
...
We are going to use it to simulate the issue described at issue #1601
2017-06-02 15:38:08 -07:00
Leonardo de Moura
92a72b238b
feat(library/tactic): add tactic::ref
...
They can be used to store user state in the tactic_state object.
@Armael @jroesch: The new file tests/lean/run/tactic_ref.lean contains a few examples.
2017-06-02 15:19:03 -07:00
Leonardo de Moura
ca5439c698
feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode
...
closes #1634
This commit also changes the semantic of `tactic.focus [tac_1, ..., tac_n]`.
It now fails if the number of goals is not `n`.
Before it would only fail if there were more tactics than goals.
@Armael: See tests/lean/run/handthen.lean for examples of the new notation.
2017-06-02 11:38:04 -07:00
Leonardo de Moura
a8173c8194
feat(library/init): heterogeneous andthen type class, and tactic.seq_focus implementation
2017-06-02 10:38:27 -07:00
Leonardo de Moura
81e97de463
feat(library/init/meta/interactive): allow metavars in the show_goal tactic
2017-06-01 19:46:38 -07:00
Leonardo de Moura
18467bd302
feat(library/init/meta/interactive): add show_goal tactic for structuring proofs in interactive tactic mode
2017-06-01 18:36:50 -07:00
Leonardo de Moura
5446df1609
feat(library/init/meta/interactive): add interactive done tactic
2017-06-01 17:28:52 -07:00
Leonardo de Moura
00aef04b81
feat(library/init/meta/rec_util): add mk_constructors_fresh_names
...
@Armael @jroesch this commit implements the
`mk_constructors_fresh_names` tactic.
The new test file has a few examples.
2017-06-01 17:04:21 -07:00
Leonardo de Moura
190d792225
feat(library/init/meta/tactic): add default parameter value
2017-06-01 16:24:36 -07:00
Gabriel Ebner
f049a3f01e
refactor(library/init/meta/has_reflect): get rid of unchecked_cast
2017-06-01 10:59:09 +02:00
Gabriel Ebner
04f9eb0b4f
refactor(library/init/meta/expr): pure Lean implementation of reflected
2017-06-01 10:17:51 +02:00
Leonardo de Moura
8b0cca57d1
fix(library/noncomputable): fixes #1631
...
This commit fixes issue #1631 . However, it is not a perfect solution.
This commit improves the predicate that checks whether a definition is
noncomputable or not. This predicate was implemented before we had
a code generator.
We should refactor the code and use the code generator to check
whether a definition is noncomputable or not. Otherwise, we will
keep finding mismatches between the predicate at noncomputable.cpp
and what the code generator implements.
2017-05-31 23:16:37 -07:00
Leonardo de Moura
42eeb445d4
fix(library): make sure `(t) does not evaluate t
...
See #1631
2017-05-31 22:03:15 -07:00
Leonardo de Moura
d8fa93b4a2
feat(library/init/meta/tactic): add dependent parameters for empty introv
2017-05-31 15:10:07 -07:00
Leonardo de Moura
1c6e70d170
feat(library/init/meta): introv tactic
...
@Armael: this commit implements the `introv` tactic.
The implementation uses an auxiliary `intros_dep` that introduces new
hypotheses with forward dependencies.
The `tactic.introv` tactic implemented at library/init/meta/tactic.lean
is the main implementation, but it is not nice for interactive use since
users would have to write
```
tactic.introv [`h1, `h2]
```
To make it more conveninent to use, we define another
```
meta def introv (ns : parse ident_*) : tactic unit :=
tactic.introv ns >> return ()
```
This one is in the namespace `tactic.interactive`, and
uses parser extensions. The argument `parse ident_*` instructs
the parser to parse 0 or more identifiers and create a term
of type `list name` containing these identifiers.
2017-05-31 14:09:25 -07:00
Leonardo de Moura
71ef240817
feat(library/init/meta/interactive): add nary existsi
...
@Armael, this commit implements the nary existsi.
We can now write
a) existsi t
b) existsi [t_1, t_2, t_3]
2017-05-31 13:41:25 -07:00
Sebastian Ullrich
9fa31b2858
fix(init/meta/interactive): handle pure in parser signature descs
2017-05-31 16:05:02 +02:00
Leonardo de Moura
72134a7bbd
feat(library/equations_compiler/wf_rec): provide recursive equations to rel_tac
...
rel_tac is a tactic used for synthesizing a well founded relation.
The default implementation just uses type class resolution.
More sophisticated strategies may need to access the set of recursive
equations. This commit addresses this need.
2017-05-30 16:55:37 -07:00
Gabriel Ebner
ddab6260aa
fix(library/init/meta/tactic): measure tactic creation time
2017-05-29 14:57:08 +02:00
Mario Carneiro
9c29206386
feat(init/meta/injection_tactic): injections tactic
...
Runs injection repeatedly on the LC and subgoals
2017-05-27 06:15:47 -04:00
Mario Carneiro
6e88119f55
feat(init/meta/injection_tactic): better injection tactic
...
(1) The lhs and rhs will be reduced to whnf before getting the constructor apps
(2) If the lhs and rhs are distinct constructors, it discharges the goal by contradiction
(3) The interactive injection tactic will try to close the goal by assumption if successful
2017-05-27 04:59:40 -04:00
Mario Carneiro
2251de503d
feat(init/relator): some new base theorems for transfer tactic
2017-05-27 04:16:25 -04:00
Mario Carneiro
57837c2b3e
fix(init/meta/tactic): let by_cases handle elimination to Type
2017-05-27 04:14:06 -04:00
Mario Carneiro
1d3887dd3f
fix(init/meta/interactive): bug in generalize2
2017-05-27 04:13:57 -04:00
Leonardo de Moura
a31e3a95ae
feat(library/equations_compiler/wf_rec): improve error message for failed decreasing proofs
2017-05-26 13:55:29 -07:00
Leonardo de Moura
62c24f9bb5
chore(*): remove pos_num and num from stdlib
2017-05-25 18:24:16 -07:00
Leonardo de Moura
0bf51e63e8
fix(library/init/meta/constructor_tactic): fixes #1598
2017-05-25 09:57:15 -07:00
Jared Roesch
191a3d662d
feat(leanpkg): add initial support for test command
2017-05-24 14:55:59 -07:00
Leonardo de Moura
1d7dd20091
feat(library/init/meta/well_founded_tactics): improve default dec_tac
...
This is a temporary workaround until we have decision procedures for arithmetic.
2017-05-24 14:34:54 -07:00
Leonardo de Moura
6ad9e3ed1e
feat(library/init/meta/well_founded_tactics): add simple tactic for discharging decreasing proofs
2017-05-23 22:07:46 -07:00
Leonardo de Moura
bebdba1004
fix(library/init/meta/simp_tactic): make sure replace_target does not fail due to reducibility settings
2017-05-23 21:43:37 -07:00
Leonardo de Moura
e163b5c884
feat(library/init/meta/expr): binder_info.other ==> binder_info.aux_decl
2017-05-23 21:42:52 -07:00
Leonardo de Moura
4fbb65d9f1
feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs
2017-05-23 15:00:29 -07:00
Sebastian Ullrich
49e5c69447
fix(init/meta/expr): have all reflected defns accept Sort
2017-05-23 11:00:33 +02:00
Gabriel Ebner
54114fd7bd
fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks
2017-05-23 07:28:34 +02:00
Sebastian Ullrich
9507297687
fix(init/meta/expr,library): reflect should accept Props
...
Fixes #1590
2017-05-19 14:17:06 +02:00
Sebastian Ullrich
84997bf4de
refactor(init/meta/expr): unify expr and pexpr
2017-05-17 10:38:12 -07:00
Leonardo de Moura
cb6d5675df
chore(library/init): ^. ==> .
2017-05-16 15:00:58 -07:00
Mario Carneiro
6b28499e47
feat(init/data/list,data/list): new basic list operations from haskell
2017-05-16 14:38:43 -07:00
Leonardo de Moura
0091cef9f2
feat(library/tactic): start algebraic normalizer
2017-05-15 21:46:19 -07:00
Leonardo de Moura
4575c9e038
feat(frontends/lean): swap (t) and ``(t) semantics
2017-05-15 09:41:31 -07:00
Mario Carneiro
7ace147f25
refactor(init/meta/tactic): replace assertv -> note, definev -> pose
2017-05-14 19:34:27 -07:00
Sebastian Ullrich
27c1d2f4fb
fix(init/meta/interactive): simp: accept local refs as simp names
2017-05-14 19:19:22 -07:00
Sebastian Ullrich
eb60df4409
fix(init/meta/interactive): case didn't find some cases
2017-05-14 19:19:22 -07:00
Sebastian Ullrich
808ab73d93
refactor(init): use list for expr.macro args
2017-05-14 19:17:28 -07:00
Sebastian Ullrich
42eb0c680e
feat(kernel/inductive,library/inductive_compiler): do not enforce positivity rule on meta inductives
2017-05-14 19:17:28 -07:00
Sebastian Ullrich
171a96a8de
refactor(library): remove all instances of `(...)
2017-05-12 19:13:48 +02:00
Sebastian Ullrich
4b21b13649
refactor(init): replace has_quote class with reflected
2017-05-09 16:02:42 -07:00
Sebastian Ullrich
ead6318ee0
feat(frontends/lean/elaborator): substitute reflected locals into expr quotes
2017-05-09 16:02:41 -07:00
