max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/frontends/lean
History
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
..
brackets.cpp fix(frontends/lean): error localization bugs 2016-10-15 13:40:57 -07:00
brackets.h feat(frontends/lean): add basic notation for collections 2016-09-21 16:20:57 -07:00
builtin_cmds.cpp fix(frontends/lean/builtin_cmds): information position (use the same approach used in other commands) 2016-11-29 16:47:34 -08:00
builtin_cmds.h refactor(*): structured message objects 2016-10-13 18:49:10 -07:00
builtin_exprs.cpp feat(frontends/lean/builtin_exprs): curly braces after show/have enter interactive mode 2016-11-18 17:00:08 -08:00
builtin_exprs.h feat(frontends/lean): generalize '~>' notation, and add alias '^.' for '~>' 2016-09-23 08:18:19 -07:00
calc.cpp refactor(kernel): reduce number of configurations supported in the kernel 2016-09-27 17:07:01 -07:00
calc.h refactor(library/relation_manager): cleanup and add API for declaring a relation that may not be reflexive, symmetric nor transitive 2015-07-07 15:58:24 -07:00
CMakeLists.txt feat(frontends, shell): implement basic server 'info' command 2016-11-08 08:37:41 -08:00
cmd_table.h refactor(frontends/decl_cmds): simplify definition parsing logic 2016-08-08 12:44:37 -07:00
decl_attributes.cpp feat(frontends/lean/decl_attributes): add 'default_priority' attribute 2016-10-01 13:27:08 -07:00
decl_attributes.h fix(frontends/lean/structure_cmd): make sure structure_cmd takes the option default_priority into account 2016-10-01 13:47:19 -07:00
decl_cmds.cpp feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction 2016-11-29 11:12:43 -08:00
decl_cmds.h chore(frontends/lean): delete old definition command 2016-09-19 16:50:25 -07:00
decl_util.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
decl_util.h fix(frontends/lean): error localization bugs 2016-10-15 13:40:57 -07:00
definition_cmds.cpp fix(frontends/lean/definition_cmds): correctly copy _refl_lemma attributes 2016-11-29 11:12:44 -08:00
definition_cmds.h feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
dependencies.cpp feat(*): add support for separate HoTT library 2014-12-05 14:34:02 -08:00
dependencies.h
elaborator.cpp fix(frontends/lean): position information for by tac 2016-11-29 17:08:10 -08:00
elaborator.h fix(frontends/lean/definition_cmds): implicit universe theorem parameters bug 2016-11-29 11:12:43 -08:00
elaborator_exception.cpp feat(frontends/lean/elaborator): improve error messages for eliminators 2016-09-29 11:29:59 -07:00
elaborator_exception.h feat(frontends/lean/elaborator): more detailed error message for a^.f notation 2016-10-18 16:22:05 -07:00
inductive_cmds.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
inductive_cmds.h feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 2016-09-29 17:56:35 -07:00
info_manager.cpp chore(*): compilation errors, fix style, fix warnings 2016-11-29 11:35:01 -08:00
info_manager.h chore(*): compilation errors, fix style, fix warnings 2016-11-29 11:35:01 -08:00
init_module.cpp chore(frontends/lean): remove dead code 2016-11-04 12:36:12 -07:00
init_module.h
json.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
json.h feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
local_context_adapter.cpp feat(frontends/lean): parse mutual_definition 2016-08-11 13:47:52 -07:00
local_context_adapter.h refactor(frontends/lean): move local_context_adapter to separate folder 2016-08-10 07:52:38 -07:00
local_decls.h fix(frontends/lean): fixes #652 2015-06-03 21:53:51 -07:00
local_level_decls.h fix(frontends/lean/builtin_cmds): redeclare_aliases 2016-03-30 16:30:18 -07:00
local_ref_info.cpp feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
local_ref_info.h fix(frontends/lean/pp): fixes #634 2015-05-29 14:07:38 -07:00
match_expr.cpp fix(frontends/lean): error localization bugs 2016-10-15 13:40:57 -07:00
match_expr.h refactor(frontends/lean): move match-expr parser to different module 2016-08-08 09:05:22 -07:00
notation_cmd.cpp chore(frontends/lean): remove dead code 2016-11-04 12:36:12 -07:00
notation_cmd.h refactor(*): remove abbreviation command 2016-09-03 17:11:29 -07:00
opt_cmd.cpp refactor(frontends/lean): implement show goal function using exceptions 2016-10-21 15:42:29 -07:00
opt_cmd.h refactor(frontends/lean): implement show goal function using exceptions 2016-10-21 15:42:29 -07:00
parse_table.cpp chore(frontends/lean): remove info_annotation module 2016-09-19 21:19:31 -07:00
parse_table.h chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
parser.cpp chore(*): compilation errors, fix style, fix warnings 2016-11-29 11:35:01 -08:00
parser.h chore(*): compilation errors, fix style, fix warnings 2016-11-29 11:35:01 -08:00
parser_config.cpp feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
parser_config.h feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
parser_pos_provider.cpp refactor(frontends/lean,library): move scope_pos_info_provider to library 2016-06-30 10:19:35 +01:00
parser_pos_provider.h refactor(frontends/lean,library): move scope_pos_info_provider to library 2016-06-30 10:19:35 +01:00
pp.cpp fix(frontends/lean/pp): char literals 2016-11-23 11:58:11 -08:00
pp.h feat(frontends/lean/pp): pretty print set_of notation 2016-09-24 13:55:02 -07:00
prenum.cpp refactor(kernel): remove extension_context 2016-03-19 15:15:39 -07:00
prenum.h checkpoint: new numeral encoding 2015-11-08 14:04:55 -08:00
print_cmd.cpp fix(frontend/lean/print_cmd): make print work with incorrect proofs 2016-11-29 11:12:43 -08:00
print_cmd.h refactor(frontends/lean): move 'print_cmd' to separate module 2015-12-28 09:08:18 -08:00
scanner.cpp feat(library,frontends/lean): add basic doc string support 2016-11-25 18:52:56 -08:00
scanner.h feat(library,frontends/lean): add basic doc string support 2016-11-25 18:52:56 -08:00
structure_cmd.cpp chore(frontends/lean): remove namespace documentation 2016-11-27 11:57:03 -08:00
structure_cmd.h feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 2016-09-29 17:56:35 -07:00
structure_instance.cpp fix(frontends/lean/structure_instance): incorrect assertions 2016-09-23 10:30:30 -07:00
structure_instance.h feat(frontends/lean): structure instances 2016-09-21 22:52:43 -07:00
tactic_notation.cpp fix(frontends/lean): position information for by tac 2016-11-29 17:08:10 -08:00
tactic_notation.h feat(frontends/lean/tactic_notation): add notation for entering auto-quotation mode 2016-09-30 16:18:52 -07:00
token_table.cpp feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction 2016-11-29 11:12:43 -08:00
token_table.h chore(library/definitional,frontends/lean): remove decreasing macro 2016-08-09 16:27:33 -07:00
tokens.cpp feat(frontends/lean/tactic_notation): allow lemmas to be removed 2016-09-30 19:53:51 -07:00
tokens.h feat(frontends/lean/tactic_notation): allow lemmas to be removed 2016-09-30 19:53:51 -07:00
tokens.txt feat(frontends/lean/tactic_notation): allow lemmas to be removed 2016-09-30 19:53:51 -07:00
type_util.cpp feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
type_util.h feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
update_environment_exception.h feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed 2015-03-13 14:47:21 -07:00
util.cpp feat(library/init/meta/tactic): universe polymorphic tactics 2016-10-25 03:42:55 +08:00
util.h fix(frontends/lean): error localization bugs 2016-10-15 13:40:57 -07:00