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 9f161e6968 fix(library,kernel): the new proj_sname field must be taken into account during comparisons 
`proj_sname` is not just for enabling better pretty printing. It is
necessary in the compiler when type information is lost, and we can't
infer the type of a `proj`-term argument (field `proj_expr`).
2018-10-03 13:11:46 -07:00
..
abstract.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
abstract.h refactor(kernel): has_local ==> has_fvar 2018-06-11 10:46:05 -07:00
cache_stack.h chore(kernel/cache_stack): compilation warning 2018-05-22 09:46:00 -07:00
CMakeLists.txt chore(kernel): move abstract_type_context to library 2018-09-08 08:29:51 -07:00
declaration.cpp feat(kernel): save constructor idx and nfields at constructor_val 2018-09-14 13:45:58 -07:00
declaration.h feat(library/compiler): eta expand quot primitives, add support for eq.rec_on 2018-09-30 08:24:18 -07:00
environment.cpp feat(kernel/type_checker): remove m_memoize 2018-09-07 20:50:53 -07:00
environment.h feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
equiv_manager.cpp chore(kernel): remove expr.quote constructor 2018-09-07 22:08:08 -07:00
equiv_manager.h chore(*): rename expr_struct_* to expr_* 2018-04-09 12:55:48 -07:00
expr.cpp feat(kernel): store structure name in proj-expressions 2018-10-02 09:23:11 -07:00
expr.h feat(kernel): store structure name in proj-expressions 2018-10-02 09:23:11 -07:00
expr_cache.cpp refactor(kernel/expr): implement expr using runtime/object 2018-06-21 16:05:33 -07:00
expr_cache.h refactor(kernel): add expr_cache 2015-02-03 14:59:55 -08:00
expr_eq_fn.cpp fix(library,kernel): the new proj_sname field must be taken into account during comparisons 2018-10-03 13:11:46 -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 chore(*): rename expr_struct_* to expr_* 2018-04-09 12:55:48 -07:00
expr_sets.h chore(*): rename expr_struct_* to expr_* 2018-04-09 12:55:48 -07:00
find_fn.h refactor(kernel/find_fn): simplify find_fn module 2014-07-23 18:09:58 -07:00
for_each_fn.cpp chore(kernel): remove expr.quote constructor 2018-09-07 22:08:08 -07:00
for_each_fn.h refactor(kernel/for_each_fn): simplify module interface 2014-07-23 18:16:41 -07:00
inductive.cpp feat(kernel): save constructor idx and nfields at constructor_val 2018-09-14 13:45:58 -07:00
inductive.h feat(kernel/inductive): inductive_reduce_rec should not throw exception when it finds an unknown constant 2018-09-07 17:34:54 -07:00
init_module.cpp chore(kernel): remove old_type_checker 2018-09-07 08:55:37 -07:00
init_module.h refactor(*): explicit initialization/finalization for serialization 2014-09-22 15:26:41 -07:00
instantiate.cpp chore(kernel): remove dummy file 2018-09-07 21:43:15 -07:00
instantiate.h feat(library/compiler/lcnf): add better support for complete-transition used in the equation compiler and x@ patterns 2018-09-20 21:38:57 -07:00
kernel_exception.h feat(library/message_builder): pretty-print kernel_exceptions 2018-09-13 16:38:40 -07:00
level.cpp chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
level.h chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
local_ctx.cpp chore(kernel/local_ctx): typo 2018-09-11 18:10:10 -07:00
local_ctx.h chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
quot.cpp feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
quot.h feat(kernel): proper constant_info and declaration objects for quot type 2018-08-28 13:46:31 -07:00
replace_fn.cpp chore(kernel): remove expr.quote constructor 2018-09-07 22:08:08 -07:00
replace_fn.h refactor(*): add runtime folder 2018-05-14 14:23:56 -07:00
type_checker.cpp feat(kernel): store structure name in proj-expressions 2018-10-02 09:23:11 -07:00
type_checker.h feat(library/compiler): eta expand definitions 2018-09-23 19:27:06 -07:00