Sebastian Ullrich
f75ce86f71
fix: server: go to type definition
2021-04-08 18:54:53 +02:00
Leonardo de Moura
2da8e5afa1
chore: add completion test for the group issue
2021-04-07 22:46:08 -07:00
Sebastian Ullrich
0396168c2c
test: make sure the interactive test would have actually failed without the fix
2021-04-07 18:05:48 +02:00
Sebastian Ullrich
5b5a882da6
fix: watchdog: do not reorder messages while delaying edits
2021-04-07 17:12:37 +02:00
Sebastian Ullrich
2de5b141eb
test: interactive: support inserting text
2021-04-07 17:12:37 +02:00
Leonardo de Moura
9b0c054258
test: auto completion
2021-04-05 20:45:04 -07:00
Leonardo de Moura
803161d9fc
fix: propagate expected type
2021-04-05 20:00:05 -07:00
Leonardo de Moura
3ccd992dad
feat: elaborate auxiliary completion node
2021-04-05 19:07:39 -07:00
Leonardo de Moura
f13bdd6869
fix: error recovery at sepBy combinator
2021-04-05 18:38:57 -07:00
Sebastian Ullrich
e863376be1
chore: simplify tests
2021-04-05 22:01:56 +02:00
Leonardo de Moura
fbd6adaf21
chore: fix tests
2021-04-05 12:35:52 -07:00
Leonardo de Moura
383e32937e
test: completion
2021-04-05 12:01:58 -07:00
Sebastian Ullrich
46be48211e
test: dot completion
2021-04-05 14:00:22 +02:00
Sebastian Ullrich
e20b2c359a
feat: server: show goal state after tactic if cursor not strictly before tactic
2021-04-03 00:23:46 +02:00
Sebastian Ullrich
ac9fee5854
test: add Lean 3-style interactive server tests
...
Fixes #376
2021-04-03 00:23:46 +02:00
Leonardo de Moura
6234c60aae
chore(*): disable test suite
2018-04-10 12:56:55 -07:00
Sebastian Ullrich
70167def6f
refactor(init/category/state): replace monad_state_lift with Haskell's MonadState
...
* does not leak information about the inner monad via out_param
* can be derived from an inner `monad_state` instance
2018-03-20 14:58:37 -07:00
Sebastian Ullrich
69cfdbd290
refactor(init/category): make all monad transformers structures, replace monad classes with has_monad_lift_t wrappers
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
c36393066e
feat(init/category): introduce monad_functor and implement it for reader, state, and except
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
788e8695eb
refactor(init/category/state): replace modify/put (returning unit) with modify'/put' (returning punit)
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
159b45c74f
refactor(init/category/state): introduce monad_state
...
* rename `read/write` to `get/put`, as in Haskell
* define `state` as `state_t id`
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
63382cf7e3
chore(init/category/transformers): move monad_transformer, monad_lift out of monad namespace, make universe polymorphic
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
703d12d594
feat(frontends/lean/elaborator): do not execute tactics after error recovery
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
67fc899d0d
feat(shell/server): sync: default "content" to file content
...
This mostly simplifies debugging and testing
2018-01-23 11:14:18 -08:00
Leonardo de Moura
040722c7e7
feat(library/init/meta): add unify config option to apply_cfg
...
This commit also fixes a problem in the `apply` tactic error messages.
2018-01-04 12:51:59 -08:00
Leonardo de Moura
f0231f17bc
feat(library/init/meta): propagate tags in constructor-like tactics
2017-12-11 16:27:03 -08:00
Leonardo de Moura
f1510a82c7
chore(tests/lean): fix tests
2017-12-10 19:30:43 -08:00
Leonardo de Moura
1b34160396
feat(library/tactic/tactic_state): display number of goals
2017-12-06 11:20:09 -08:00
Floris van Doorn
52ee29cb48
fix(interactive): fix focus tactic.
...
Previously it would fail if there was more than one goal.
2017-11-03 12:58:48 -07:00
Jeremy Avigad
bcad5309d9
fix(library/init/meta/interactive): implement docstring fixes from kha
2017-09-22 16:53:22 -04:00
Jeremy Avigad
57f9cbeb78
fix(tests/lean/interactive/*): fix tests
2017-09-21 21:16:20 -04:00
Leonardo de Moura
51bac2918f
chore(library/init/core): declare and using structure
...
This change was requested by several users.
2017-09-05 15:08:20 -07:00
Gabriel Ebner
ce509e621a
refactor(library/init/algebra): remove order_pair classes
2017-08-02 14:41:35 +01:00
Mario Carneiro
ec82afb45a
fix(tests): fix tests
2017-07-28 16:47:02 +01:00
Mario Carneiro
94ecc3292f
fix(tests): fix tests
2017-07-21 02:10:48 -07:00
Sebastian Ullrich
f8cfc4ea1b
feat(kernel/error_msgs,frontends/lean/elaborator): add more context to 'type/function expected' errors
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
2bfdcc9069
chore(tests/lean/interactive/info_tactic): make independent of stdlib tactics
2017-07-07 11:22:12 +02:00
Sebastian Ullrich
99a87a9d01
chore(tests/lean/interactive/complete_field): remove. Not supported with new field notation anyway.
2017-07-07 11:22:10 +02:00
Gabriel Ebner
f55d10bb50
chore(tests/lean/interactive): fix tests
2017-07-06 16:32:50 +02:00
Jeremy Avigad
5fd113f50f
feat(library/init/logic): add simp rule for 'true implies p'
2017-07-05 14:26:04 -07:00
Leonardo de Moura
bb9e3ddae2
feat(library/init/meta/interactive): rw [-h] ==> rw [← h]
...
@Armael: this change may affect your project.
The file `doc/changes.md` explains the motivation for the change.
2017-07-05 11:42:55 -07:00
Leonardo de Moura
b68fe0d645
chore(tests/lean/interactive): fix test
2017-07-04 11:57:16 -07:00
Leonardo de Moura
b86847ec72
fix(library/init/logic): mark eq.substr with [elab_as_eliminator]
...
See issue #1718
2017-07-03 17:27:41 -07:00
Leonardo de Moura
e24f3341d4
feat(library/init/meta/interactive): simp without foo ==> simp [-foo]
...
This commit also adds "exception" validation.
A bad "exception" was being silently ignored.
We can also exclude hypotheses. Example: `simp [*, -h]`
2017-07-03 17:10:46 -07:00
Leonardo de Moura
76799db032
feat(library/init/meta/interactive): simph ==> simp [*]
...
This modification was suggested by @kha.
TODO:
- Use `simp [-f]` instead of `simp without f`
- Allow users to remove hypothesis from `*`. Example: `simp [*, -h]`
for simplify using all hypotheses but `h`.
2017-07-03 15:14:47 -07:00
Leonardo de Moura
16711fcdba
feat(library/tactic/dsimplify): new configuration options for dsimp
...
TODO for `dsimp`:
- Add an option for reducing [reducible] definitions
- Add (to_unfold : list name) similar to the one in the `simp` tactic
2017-07-02 18:26:03 -07:00
Leonardo de Moura
0b36e014e6
chore(tests/lean): fix tests
2017-07-01 21:12:29 -07:00
Leonardo de Moura
4604d7fd5a
feat(library/init/meta): allow users to specify tactic for discharging subgoals in the simp tactic family
...
@dselsam @Armael: this feature may be useful for you.
The doc/changes.md describes many other new features.
2017-07-01 15:35:33 -07:00
Leonardo de Moura
2f2694a343
chore(tests/lean/interactive/info_tactic): fix test output
2017-07-01 13:11:07 -07:00
Leonardo de Moura
b05c4e09ed
feat(library/init/meta): add memoize field to simp_config and dsimp_config
...
We use `memoize := ff` when implementing `conv.interactive.for` and
`conv.interactive.find`.
2017-07-01 10:37:09 -07:00
