max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/kernel
History
Leonardo de Moura 88cd294a09 feat(src/kernel/error_msgs): show aliased variables when printing error messages 
closes #1814

@kenmcmil: the error messages will now list aliased variables.
For example, in your file, the new error message is:

```
invalid type ascription, term has type
  triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
but is expected to have type
  triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
types contain aliased name(s): c'
remark: the tactic `dedup` can be used to rename aliases
state:
...
```
2017-09-05 16:46:44 -07:00
..
inductive fix(kernel/inductive/inductive): identify indices modulo whnf 2017-07-06 20:59:58 -07:00
quotient chore(kernel/quotient/quotient): update comments 2017-03-07 14:11:51 -08:00
abstract.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
abstract.h fix(frontends/lean/structure_cmd): remove evil Pi overload that accidentally abstracted constants in structure decls 2017-04-26 14:22:36 -07:00
abstract_type_context.cpp fix(frontends/lean/pp): qualify constant shadowed by local 2017-03-31 09:40:49 -07:00
abstract_type_context.h fix(frontends/lean/pp): qualify constant shadowed by local 2017-03-31 09:40:49 -07:00
cache_stack.h perf(kernel/for_each_fn): use cache stack trick at for_each_fn 2014-07-23 19:32:11 -07:00
CMakeLists.txt refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
declaration.cpp refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
declaration.h refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
environment.cpp refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
environment.h chore(kernel/environment): rename method 2017-05-15 14:18:16 -07:00
equiv_manager.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
equiv_manager.h feat(kernel/equiv_manager): use expr_struct_map in the equiv_manager 2016-07-07 07:39:25 -07:00
error_msgs.cpp feat(src/kernel/error_msgs): show aliased variables when printing error messages 2017-09-05 16:46:44 -07:00
error_msgs.h feat(frontends/lean/elaborator): closes #1760 2017-08-21 16:15:03 -07:00
expr.cpp fix(kernel/expr,library/constructions/projection): preserve instance-implicitness in structure parameters 2017-08-27 16:47:04 +02:00
expr.h feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
expr_cache.cpp refactor(kernel): add expr_cache 2015-02-03 14:59:55 -08:00
expr_cache.h refactor(kernel): add expr_cache 2015-02-03 14:59:55 -08:00
expr_eq_fn.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
expr_eq_fn.h feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information 2016-08-01 16:34:07 -07:00
expr_maps.h feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information 2016-08-01 16:34:07 -07:00
expr_pair.h feat(library/type_context, frontends/lean/elaborator): type classes with output parameters 2017-01-30 18:32:54 -08:00
expr_sets.h perf(kernel/expr_eq_fn): use thread local cache, and avoid memory allocation/deallocation 2014-10-17 16:44:20 -07:00
ext_exception.h chore(util,kernel,library): clang warnings 2017-02-17 20:01:34 -08:00
find_fn.h refactor(kernel/find_fn): simplify find_fn module 2014-07-23 18:09:58 -07:00
for_each_fn.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
for_each_fn.h refactor(kernel/for_each_fn): simplify module interface 2014-07-23 18:16:41 -07:00
formatter.cpp fix(*): remove unnecessary null pointer checks 2015-03-28 12:16:39 -07:00
formatter.h feat(library/type_context): better error messages 2016-09-28 15:59:43 -07:00
free_vars.cpp feat(kernel): add compilation flag for disabling "free var range" optimization 2017-02-21 19:40:56 -08:00
free_vars.h refactor(kernel/expr): remove dead code 2014-10-16 13:09:26 -07:00
init_module.cpp fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
init_module.h refactor(*): explicit initialization/finalization for serialization 2014-09-22 15:26:41 -07:00
instantiate.cpp feat(kernel): add compilation flag for disabling "free var range" optimization 2017-02-21 19:40:56 -08:00
instantiate.h feat(kernel/instantiate): add helper function 2016-08-14 16:16:03 -07:00
kernel_exception.cpp feat(frontends/lean/elaborator): closes #1760 2017-08-21 16:15:03 -07:00
kernel_exception.h fix(library/tactic/eval,kernel/kernel_exception): hide internal definition name on eval_expr type error 2017-03-27 13:42:08 -07:00
level.cpp fix(kernel/expr): disable caching by default 2017-03-23 08:57:56 +01:00
level.h feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
normalizer_extension.cpp refactor(kernel): remove extension_context 2016-03-19 15:15:39 -07:00
normalizer_extension.h refactor(kernel): remove extension_context 2016-03-19 15:15:39 -07:00
pos_info_provider.cpp refactor(*): use + for concatenating format objects 2014-08-24 09:35:25 -07:00
pos_info_provider.h feat(kernel/pos_info_provider): add save_pos_info 2017-03-31 09:40:48 -07:00
replace_fn.cpp fix(kernel/replace_fn): check if running out of stack space at replace_rec_fn 2017-06-04 15:57:11 -07:00
replace_fn.h feat(kernel/replace_fn): add use_cache flag to replace function 2015-02-05 10:49:18 -08:00
scope_pos_info_provider.cpp refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
scope_pos_info_provider.h refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
standard_kernel.cpp refactor(library/standard_kernel): move standard kernel into kernel 2017-01-31 09:39:31 +01:00
standard_kernel.h refactor(library/standard_kernel): move standard kernel into kernel 2017-01-31 09:39:31 +01:00
type_checker.cpp feat(frontends/lean/elaborator): closes #1760 2017-08-21 16:15:03 -07:00
type_checker.h chore(kernel/type_checker): remove dead code 2017-02-15 18:05:55 -08:00