Leonardo de Moura
f96d35dc1c
fix(library/aux_definition,frontends/lean/definition_cmds): unfold macros at trust level 0
2016-12-05 13:08:12 -08:00
Leonardo de Moura
e11fd8820a
refactor(library/init): create init.data folder
2016-12-02 14:23:06 -08:00
Leonardo de Moura
e237109434
fix(frontends/lean/tactic_notation): do not store position information for auxiliary terms introduced by the interactive mode
...
The idea is to prevent unwanted type information at lean-mode.
For example, before this commit, we would get "list.nil : ..." type
info whenever we hovered over the "end" of a "begin...end" block.
2016-12-02 09:53:24 -08:00
Leonardo de Moura
e1a90fbe89
fix(frontends/lean/tactic_notation): fixes #1207
2016-12-01 17:16:22 -08:00
Leonardo de Moura
8defd9ac39
fix(frontends/lean/elaborator): compilation warning with clang
2016-12-01 16:10:07 -08:00
Leonardo de Moura
d454cc8bcd
feat(frontends/lean/elaborator): do not populate info_manager during thread finalization
2016-11-30 17:14:15 -08:00
Gabriel Ebner
000d97a9a6
fix(frontends/lean/parser): wrap snapshot in shared_ptr
2016-11-30 11:27:02 -05:00
Gabriel Ebner
c3f72ec0d8
fix(library/module_mgr): do not copy module_info
2016-11-30 11:26:59 -05:00
Leonardo de Moura
2309e35296
fix(frontends/lean): position information for by tac
...
Now, Ctrl-c-Ctrl-g also works when hovering the beginning of the tactic
instead of the beginning of the `by` token.
The idea is to make the behavior consistent with `begin...end` blocks.
2016-11-29 17:08:10 -08:00
Leonardo de Moura
b85ccefbff
fix(frontends/lean/builtin_cmds): information position (use the same approach used in other commands)
2016-11-29 16:47:34 -08:00
Leonardo de Moura
d40e97b4bc
chore(*): compilation errors, fix style, fix warnings
2016-11-29 11:35:01 -08:00
Gabriel Ebner
df635b56af
fix(frontends/lean/definition_cmds): correctly copy _refl_lemma attributes
2016-11-29 11:12:44 -08:00
Gabriel Ebner
3ecfddcbd5
fix(*): fix build
2016-11-29 11:12:43 -08:00
Gabriel Ebner
e448e4e129
refactor(util/task_queue): merge module_task into task and cancel by position
2016-11-29 11:12:43 -08:00
Gabriel Ebner
aa03dc03b4
refactor(library/tactic/simp_lemmas): mark rfl-lemmas with a _refl_lemma attribute
2016-11-29 11:12:43 -08:00
Gabriel Ebner
e1cb1a8cd2
feat(util/task_queue,library/versioned_msg_buf): rudimentary support for task interruption
2016-11-29 11:12:43 -08:00
Gabriel Ebner
56f895d6d8
feat(kernel/type_checker): option to disable delayed proof-checking
2016-11-29 11:12:43 -08:00
Leonardo de Moura
78608a37e9
fix(frontends/lean/definition_cmds): implicit universe theorem parameters bug
...
See discussion at #1178
2016-11-29 11:12:43 -08:00
Gabriel Ebner
7d6e71aa59
fix(frontend/lean/print_cmd): make print work with incorrect proofs
2016-11-29 11:12:43 -08:00
Gabriel Ebner
385ea13688
feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction
2016-11-29 11:12:43 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
002c62b49c
feat(frontends/lean): basic leandoc tool
2016-11-27 14:31:31 -08:00
Leonardo de Moura
94c882f4d5
feat(library/documentation, frontends/lean): add /-! -/ doc string module block
2016-11-27 12:23:53 -08:00
Leonardo de Moura
6978906a78
chore(frontends/lean): remove namespace documentation
...
We will add module level doc strings /-! -/
2016-11-27 11:57:03 -08:00
Leonardo de Moura
338a46c225
fix(library/documentation): do not store doc strings for namespaces and declarations in the same name_map
2016-11-26 09:41:07 -08:00
Leonardo de Moura
97dd2f34d5
feat(library,frontends/lean): add basic doc string support
2016-11-25 18:52:56 -08:00
Leonardo de Moura
0554fd5997
fix(frontends/lean): name resolution at tactic execution time
...
This commit also adds a new tactic: tactic.resolve_name
closes #1201
2016-11-24 10:55:39 -08:00
Leonardo de Moura
701fa0d1f4
fix(frontends/lean/builtin_cmds): make sure declarations generated by run_command get line/col info
2016-11-24 09:21:49 -08:00
Leonardo de Moura
ffe9b3c5d6
fix(frontends/lean/pp): char literals
2016-11-23 11:58:11 -08:00
Leonardo de Moura
9d52b6607d
feat(library/tactic): use annotated_head_beta_reduce instead of head_beta_reduce in tactics
2016-11-21 15:40:12 -08:00
Leonardo de Moura
e17b3df16a
fix(frontends/lean/elaborator): bad error message
2016-11-21 12:18:31 -08:00
Leonardo de Moura
ed2a507dd9
fix(frontends/lean/tactic_notation): assertion violation
2016-11-18 17:39:25 -08:00
Leonardo de Moura
f02de7e380
feat(frontends/lean/builtin_exprs): curly braces after show/have enter interactive mode
2016-11-18 17:00:08 -08:00
Leonardo de Moura
88d2f07567
feat(frontends/lean/tactic_notation): switch to proof-term mode when calc/suppose/assume/have/show occurs in a tactic block
2016-11-18 16:57:31 -08:00
Leonardo de Moura
d59bf05f20
feat(frontends/lean/scanner): allow ' in the beginning of identifiers
2016-11-17 11:53:21 -08:00
Leonardo de Moura
dfd2a23cd4
feat(frontends/lean): use #"c" instead of 'c' for character literals
...
The new notation is the same one used in Standard ML.
It will also allow us to use ' in the beginning of identifiers like Standard ML.
2016-11-17 11:35:54 -08:00
Leonardo de Moura
e16e9880f7
chore(library/system): enforce Lean naming conventions IO ==> io
2016-11-17 11:27:37 -08:00
Leonardo de Moura
b0d6d171be
feat(library/tactic/vm_monitor): add basic io support for VM monad
2016-11-15 18:42:14 -08:00
Leonardo de Moura
7232e3a076
feat(library/vm/vm): invoke debugger (aka vm_monitor)
2016-11-14 14:45:49 -08:00
Leonardo de Moura
b59c10118d
fix(*): memory leaks
2016-11-11 11:56:54 -08:00
Leonardo de Moura
1a8b582533
fix(frontends/lean/info_manager): uninitialized variable
2016-11-11 11:50:05 -08:00
Leonardo de Moura
714b780636
feat(frontends/lean/elaborator): save type info for let-exprs
2016-11-10 16:34:48 -08:00
Leonardo de Moura
d95645bd89
feat(frontends/lean/elaborator): save type information for binders
2016-11-10 15:39:38 -08:00
Sebastian Ullrich
2a37611d1f
feat(emacs): implement show-goal-at-pos using faster info manager
2016-11-10 15:17:15 -08:00
Leonardo de Moura
922d48524b
fix(frontends/lean): fixes #1188
...
This commit also adds support for recording the type of local variables
in the info_manager
2016-11-10 15:08:25 -08:00
Leonardo de Moura
29e5464e42
fix(frontends/lean/tactic_notation): fix minor problem for info at position
...
See comment for details.
2016-11-10 13:48:35 -08:00
Leonardo de Moura
40fca8efd4
feat(frontends/lean): add tactic.save_type_info, preserve pos info at translate
2016-11-10 11:51:05 -08:00
Leonardo de Moura
83e0e7104c
feat(frontends/lean): save tactic_state in the info_manager
2016-11-10 09:56:36 -08:00
Leonardo de Moura
d6000416f8
feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information
...
We will use this information in the debugger.
2016-11-09 16:51:48 -08:00
Gabriel Ebner
a3aced1b30
feat(frontends/lean/structure_cmd): record position of structure declaration
2016-11-08 19:22:42 -08:00
