Sebastian Ullrich
ed4275ae17
fix(frontends/lean/builtin_cmds): do not complete after namespace
...
Most identifiers used with the command are not namespaces yet
2017-01-10 14:42:48 -08:00
Sebastian Ullrich
8eb39bb982
fix(frontends/lean/parser): catch exceptions thrown by sync_command
2017-01-10 14:42:48 -08:00
Leonardo de Moura
00c89f209c
fix(frontends/lean/definition_cmds): fix #1299
2017-01-10 14:38:46 -08:00
Sebastian Ullrich
3ae4d0fbee
feat(shell/completion,emacs/lean-company): provide doc string and location with completion candidate
2017-01-10 16:19:32 +01:00
Sebastian Ullrich
cc3126e944
feat(frontends/lean,library/scoped_ext,shell): complete namespaces
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
b04df04120
feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes
2017-01-10 12:25:33 +01:00
Leonardo de Moura
7a150b41b9
fix(frontends/lean): fixes #1292
2017-01-09 15:53:37 -08:00
Leonardo de Moura
7d540b6d02
fix(frontends/lean/parser): fixes #1290
2017-01-09 15:35:25 -08:00
Leonardo de Moura
299751982b
fix(frontends/lean/tactic_evaluator): 'begin [smt] ... end' block nested in regular one
2017-01-07 13:35:43 -08:00
Leonardo de Moura
93c8e69313
chore(frontends/lean, library): cleanup anonymous instance management
2017-01-06 14:37:44 -08:00
Sebastian Ullrich
26e2aeec7a
feat(frontends/lean,shell): complete attributes
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
2816d3a036
feat(frontends/lean,shell): complete interactive tactics
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
7040844f9a
feat(frontends/lean/parser,shell): complete imports
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
3136f36ed6
fix(frontends/lean/parser): complete after periods trailing identifiers
2017-01-06 14:02:31 -08:00
Leonardo de Moura
db70c78704
feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names
2017-01-06 11:40:34 -08:00
Leonardo de Moura
31a0d7d520
feat(frontends/lean/elaborator): catch exception at is_def_eq
...
@semorrison this commit improves the bad error message you have
reported at lean-user. It is not perfect since the user has to
remember the position of the structure field in the constructor.
2017-01-06 08:16:51 -08:00
Leonardo de Moura
7ba889b5cf
feat(frontends/lean/tactic_notation): try/repeat for smt_tactic in interactive mode
2017-01-05 18:31:57 -08:00
Gabriel Ebner
063130ee18
feat(kernel/environment): add function that checks whether all proofs are correct
2017-01-05 18:09:28 -08:00
Gabriel Ebner
90ab29d7a3
chore(CMakeLists): rename misleading LEAN_SERVER option
2017-01-05 18:08:59 -08:00
Leonardo de Moura
82f8eeb280
feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler
2017-01-05 18:02:14 -08:00
Leonardo de Moura
eeab242595
feat(frontends/lean/elaborator): catch error early
2017-01-05 13:37:55 -08:00
Leonardo de Moura
b0de6723ec
feat(frontends/lean/tactic_evaluator): better error message
2017-01-05 13:32:59 -08:00
Gabriel Ebner
9435762643
fix(compiler/vm_compiler): only compile computable non-builtin definitions
2017-01-04 16:30:22 -08:00
Leonardo de Moura
eeb8237b04
feat(frontends/lean): 'begin [smt] ... end' blocks nested inside regular 'begin ... end' blocks
2017-01-04 15:35:46 -08:00
Leonardo de Moura
2e15304f05
feat(frontends/lean): add support for smt_state in the info_manager
2017-01-04 14:23:48 -08:00
Leonardo de Moura
5f2b247af9
feat(frontends/lean/tactic_evaluator): step-by-step evaluation for 'begin [smt] ... end' blocks
2017-01-04 14:06:44 -08:00
Leonardo de Moura
d53215a2fb
feat(frontends/lean/tactic_notation, library/init/meta/smt): add by_cases and by_contradiction smt_tactics, support for classical reasoning, add support for 'begin [smt] with config, ... end'
2017-01-04 12:03:45 -08:00
Leonardo de Moura
59f3c9775a
feat(frontends/lean/tactic_notation): add support for begin [smt] ... end blocks
...
TODO: add support for inspecting intermediate states.
2017-01-04 11:13:00 -08:00
Leonardo de Moura
3a62ca0581
refactor(library/init/meta): move smt tactics to library/init/meta/smt, and add interactive definitions
2017-01-04 09:36:50 -08:00
Leonardo de Moura
d6ab3739ff
refactor(frontends/lean/elaborator): move tactic executation code to tactic_evaluator
2017-01-04 08:42:59 -08:00
Leonardo de Moura
0319fd5728
refactor(frontends/lean/elaborator): move pos_string_for
2017-01-04 07:32:44 -08:00
Leonardo de Moura
d24577c57c
fix(frontends/lean/tactic_notation): remove problematic code for get_begin_end_block_elements
2017-01-03 22:38:03 -08:00
Leonardo de Moura
e6f6c6bb3a
fix(frontends/lean/tactic_notation): typo
2017-01-03 22:15:22 -08:00
Leonardo de Moura
493be76afe
feat(frontends/lean/tactic_notation): add support for other tactic types
...
TODO: we still need to add support in the elaborator.
2017-01-03 22:11:45 -08:00
Leonardo de Moura
46a3aacc17
fix(frontends/lean): begin...end block scope
2017-01-03 21:01:14 -08:00
Leonardo de Moura
c904437d57
fix(frontends/lean/elaborator): crash when elaborating invalid structure instance
2017-01-03 11:04:14 -08:00
Leonardo de Moura
abb63cbfa6
fix(frontends/lean/elaborator): cactch app_exception when trying to create coercion
...
closes #1279
2017-01-03 09:03:00 -08:00
Leonardo de Moura
4db7c05fb8
feat(frontends/lean/elaborator): generalize try_monad_coercion
2017-01-01 14:50:01 -08:00
Leonardo de Moura
a44a975388
feat(library/type_context,frontends/lean/elaborator): add class_exception (for max depth reached), ignore them during coercion resolution (just add a trace message)
2017-01-01 08:51:09 -08:00
Leonardo de Moura
66bc3c796a
feat(frontends/lean/elaborator): add extra coercion resolution rule for monads
...
We also removed the notation (♯tac) since it is not needed anymore.
@gebner, the comment at elaborator.cpp explains why you had to use the ♯
notation. The workaround is a little bit hackish, but I think it is
worth it. We will use monad lifts in many different places.
2016-12-31 13:50:15 -08:00
Leonardo de Moura
fd4fffea27
chore(frontends/lean/info_manager): cleanup old code
2016-12-30 18:59:15 -08:00
Leonardo de Moura
5f87ec3356
feat(library/tactic): allow user to write their own pretty printer for tactic states
2016-12-30 18:58:50 -08:00
Leonardo de Moura
5d825483c4
refactor(library/init/meta/interactive): tactic.interactive.types ==> interactive.types
...
Motivation: we will use auto-quotation for other tactic monads
2016-12-30 18:06:41 -08:00
Leonardo de Moura
9c069a3eda
refactor(library/tactic/congruence): rename directory to smt
2016-12-30 13:15:19 -08:00
Leonardo de Moura
85b98f08e9
fix(frontends/lean): bad position at spurious 'end' token
2016-12-29 19:51:36 -08:00
Sebastian Ullrich
98398b16f3
feat(frontends/lean,shell): implement completing options
2016-12-27 21:41:02 -08:00
Sebastian Ullrich
daf839e0d5
feat(frontends/lean,shell/server): report current goal anywhere within begin-end/by
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
5cb06ea912
perf(frontends/lean/parser): break at break_at_pos even if not on an interesting token
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
47e7df9b27
perf(frontends/lean/definition_cmds): skip definition elaboration during reparsing
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
8ccf28abf3
chore(*): remove old code
2016-12-27 10:07:34 -08:00
