lean4-htt/src/kernel
2021-09-20 18:41:46 +02:00
..
abstract.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
abstract.h chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
cache_stack.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
CMakeLists.txt
declaration.cpp chore: remove dead code 2021-01-05 18:36:27 -08:00
declaration.h chore: disable the kernel "tryHeuristic" for abbreviations 2021-07-23 12:10:16 -07:00
environment.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
environment.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
equiv_manager.cpp chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
equiv_manager.h
expr.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
expr.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
expr_cache.cpp
expr_cache.h
expr_eq_fn.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
expr_eq_fn.h
expr_maps.h
expr_sets.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
find_fn.h
for_each_fn.cpp chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
for_each_fn.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
inductive.cpp chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
inductive.h feat: string literal support on recursors and kernel isDefEq 2020-03-17 17:23:33 -07:00
init_module.cpp
init_module.h
instantiate.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
instantiate.h chore: remove instance cache 2020-07-08 09:40:34 -07:00
kernel_exception.h
level.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
level.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
local_ctx.cpp chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
local_ctx.h fix: nonoptimal specialization 2020-09-24 12:40:28 -07:00
quot.cpp fix: binder name 2021-08-26 11:11:37 -07:00
quot.h
replace_fn.cpp chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
replace_fn.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
type_checker.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
type_checker.h perf: change is_def_eq_proof_irrel type to lbool 2021-07-26 07:11:55 -07:00