Joachim Breitner db7a01d126 chore: update comments in kernel/declaration.h (#4683) ... This file has comments that recall the data type definitions in Lean. Most of them were still using lean3 syntax, and at least one of them was out of date (one field missing), so I updated them. I took the liberty to shorten the comments from the original file, or omit them if they don’t add much over the field names.		2024-07-08 14:39:43 +00:00
..
abstract.cpp	feat: generalize Expr.abstractRange	2022-03-08 18:19:17 -08:00
abstract.h
cache_stack.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
CMakeLists.txt	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
declaration.cpp	fix: mismatch between TheoremVal in Lean and C++ (#4035)	2024-04-30 18:10:20 +00:00
declaration.h	chore: update comments in kernel/declaration.h (#4683)	2024-07-08 14:39:43 +00:00
environment.cpp	fix: adapt kernel interruption to new cancellation system (#4584)	2024-07-01 14:52:42 +00:00
environment.h	feat: collect kernel diagnostic information (#4082)	2024-05-06 21:53:16 +00:00
equiv_manager.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
equiv_manager.h
expr.cpp	perf: implement Expr.update* in Lean	2022-07-19 05:55:13 -07:00
expr.h	chore: remove remnants of C++ format	2022-11-18 06:11:24 -08:00
expr_cache.cpp
expr_cache.h
expr_eq_fn.cpp	fix: switch to C++ interruption whitelist	2023-10-26 08:33:09 +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	fix: remove unguarded check_interrupted call	2023-10-26 08:33:09 +02:00
for_each_fn.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
inductive.cpp	feat: collect kernel diagnostic information (#4082)	2024-05-06 21:53:16 +00:00
inductive.h	fix: do not apply eta for structures in Prop	2022-03-01 09:00:46 -08:00
init_module.cpp	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
init_module.h
instantiate.cpp	refactor: instantiateTypeLevelParams in Lean	2022-10-24 12:23:13 -07:00
instantiate.h
kernel_exception.h	feat: type of theorems must be propositions	2024-03-13 12:37:58 -07:00
level.cpp	chore: remove remnants of C++ format	2022-11-18 06:11:24 -08:00
level.h	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
local_ctx.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
local_ctx.h
quot.cpp	fix: binder name	2021-08-26 11:11:37 -07:00
quot.h	fix: quot reduction bug	2023-10-11 21:25:34 -07:00
replace_fn.cpp	fix: switch to C++ interruption whitelist	2023-10-26 08:33:09 +02:00
replace_fn.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
trace.cpp	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
trace.h	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
type_checker.cpp	feat: safe exponentiation (#4637)	2024-07-03 05:12:53 +00:00
type_checker.h	feat: safe exponentiation (#4637)	2024-07-03 05:12:53 +00:00