Leonardo de Moura
cd624dda75
fix(library/tactic/exact_tactic): make sure exact/refine tactics check for cycles when assigning metavariables
...
fixes #1638
2017-06-04 15:10:42 -07:00
Gabriel Ebner
86f4c9a794
fix(util/thread): disable thread finalizer manager finalization due to race condition
2017-06-04 23:29:34 +02:00
Leonardo de Moura
02c82ac41a
fix(library/tactic/tactic_state): make sure mk_unify_exception is not compiler implementation dependent
2017-06-04 13:29:59 -07:00
Jeremy Avigad
4592210e10
fix(tests/lean/*): fix and expand tests
2017-06-04 13:23:26 -07:00
Jeremy Avigad
c68326ac14
feat(library/init/meta/interactive): update simp docstring
2017-06-04 13:23:26 -07:00
Jeremy Avigad
dedc87fa7e
refactor(library/init/meta/simp_tactic): include defaults for 'simp with'
2017-06-04 13:23:26 -07:00
Jeremy Avigad
650870fd0e
fix(tests/lean/interactive/*): fix tests
2017-06-04 13:23:26 -07:00
Jeremy Avigad
d045042ae7
refactor(library/init/meta/interactive): remove special printing of loc, style fixes
2017-06-04 13:23:26 -07:00
Jeremy Avigad
c09aa24977
refactor(library/init/meta/interactive): make mk_simp_set public
2017-06-04 13:23:26 -07:00
Jeremy Avigad
ee5f00d3d0
feat(library/init/meta/simp_tactic): make simp_at return new hypothesis
2017-06-04 13:23:26 -07:00
Jeremy Avigad
c2df664c39
feat(library/init/meta/tactic): make tactics that introduce a local constant return the expr
2017-06-04 13:23:26 -07:00
Jeremy Avigad
4f2cd6d2c7
fix(tests/lean/run/simp_options): move test
2017-06-04 13:23:26 -07:00
Jeremy Avigad
7fe0fff91d
feat(library/init/meta/interactive): add 'only' option for simp, dimph, dimp_intros, and dsimp
2017-06-04 13:23:26 -07:00
Jeremy Avigad
862d23f6b6
fix(library/init/meta/interactive): disallow wildcard in rewrite
2017-06-04 13:23:26 -07:00
Jeremy Avigad
e1c024d4d9
fix(library/init/meta/simp_tactic): fix relabeling of hypotheses in simp_intro_aux
2017-06-04 13:23:26 -07:00
Jeremy Avigad
4160f23847
fix(library/init/meta/interactive): fix printing of description string for locations
2017-06-04 13:23:26 -07:00
Jeremy Avigad
1fa7c2285e
fix(library/init/meta/smt/interactive): adapt to wildcards in locations
2017-06-04 13:23:26 -07:00
Jeremy Avigad
649118c99a
fix(library/init/meta/interactive): remove sorry in dunfold_occs
2017-06-04 13:23:26 -07:00
Jared Roesch
e63f202aed
chore(tests/lean): add tests for rw and simp
2017-06-04 13:23:26 -07:00
Jared Roesch
998f90b849
feat(library/init/meta/interactive): add support for location wildcards
...
This allows users to now use to apply a tactic in all hypotheses as well as the goal, we add support for all
interactive tactics using location: rewrite, simp, dsimp, unfold, and delta including each tactics many variants.
2017-06-04 13:23:26 -07:00
Leonardo de Moura
e22ccb4d1f
feat(library/tactic/tactic_state): improve error message for unify and is_def_eq tactics
...
closes #1639
2017-06-03 19:52:22 -07:00
Sebastian Ullrich
355dac2cd1
chore(.appveyor.yml): separate upgrading and installing new packages
2017-06-03 17:42:48 +02:00
Gabriel Ebner
0c90e97134
fix(util/lp): fix compile error due to missing functions
2017-06-03 15:44:22 +02:00
Gabriel Ebner
9a706daf12
chore(util/debug): mark assertion failures as LEAN_UNLIKELY
2017-06-03 15:44:22 +02:00
Gabriel Ebner
88a1067435
fix(util/debug): extract exit-to-debugger functionality
2017-06-03 15:44:22 +02:00
Gabriel Ebner
910d63d314
refactor(util/compiler_hints): move LEAN_UNLIKELY macro out of vm code
2017-06-03 15:44:22 +02:00
Gabriel Ebner
d46c8b96fe
fix(CMakeLists): enable debugging assertions in RelWithDebInfo builds
2017-06-03 15:30:01 +02:00
Gabriel Ebner
d394654490
feat(util/debug): throw exceptions for failed assertions in server mode
2017-06-03 15:29:37 +02:00
Leonardo de Moura
a1dc121eee
feat(library/init/meta/environment): add environment.fingerprint API
2017-06-02 16:52:40 -07:00
Leonardo de Moura
6af3084f9a
feat(util/numerics/mpz): add mpz(uint64) constructor
2017-06-02 16:36: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
d7ab5cd8a1
feat(frontends/lean/tactic_notation): allow show keyword to be used as syntax sugar for the show_goal tactic
...
@kha @gebner I added the `show_goal` tactic for selecting arbitrary
subgoals. This feature is similar to the one available in Isabelle.
This commit allows us to use the `show` keyword as syntax sugar for
`show_goal`. The test `show_goal.lean` has a small example.
What do you think?
@Armael: you can use `show` to structure your proofs in tactic mode.
See `tests/lean/run/show_goal.lean` for a small example.
2017-06-01 18:52:54 -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
Mario Carneiro
d82b8ed59e
feat(init/data/int,init/data/nat,init/algebra): more algebra theorems
2017-06-01 15:15:40 -07:00
Leonardo de Moura
d8f03082b7
chore(library/type_context): style
2017-06-01 13:47:10 -07:00
Leonardo de Moura
9c79b361dc
fix(library/type_context): non deterministic failure at bitwise.lean
...
We were getting the following error non deterministically:
```
library/init/data/nat/bitwise.lean:131:6: error: exact tactic failed, type mismatch, given expression has type
z = f ff 0 z
but is expected to have type
eq.rec z e = f ff 0 (binary_rec f z 0)
state:
C : ℕ → Sort u,
f : Π (b : bool) (n : ℕ), C n → C (bit b n),
z : C 0,
h : f ff 0 z = z,
b : bool,
n : ℕ,
b0 : bit b n = 0,
bf : bodd 0 = b,
n0 : shiftr 0 1 = n,
e : 0 = bit ff 0
⊢ eq.rec z e = f ff 0 (binary_rec f z 0)
```
This error was happening because of the type_context.unfold_lemmas new
flag. The type context thread local cache must be flushed whenever the
value of type_context.unfold_lemmas has changed.
2017-06-01 13:39:12 -07:00
Leonardo de Moura
291b61555a
chore(library/type_context): add flag for disabling cache at compilation time
2017-06-01 13:32:09 -07:00
Gabriel Ebner
9aeda60e2c
fix(library/equations_compiler/util): segfault
2017-06-01 16:58:00 +02:00
Sebastian Ullrich
09987df06e
fix(frontends/lean/structure_cmd): do not collect m_ctx_locals multiple times
2017-06-01 07:38:30 -07:00
Sebastian Ullrich
1977b5bfc9
refactor(frontends/lean/structure_cmd): also simplify collecting ctx levels
2017-06-01 07:38:30 -07:00
Sebastian Ullrich
25152bc80d
fix(frontends/lean/structure_cmd): use collect_implicit_locals to catch more context locals
...
Fixes #1623
2017-06-01 07:38:30 -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
