Joshua Seaton a9317760e7 chore: update IR interpreter enum hygiene ... This change addresses -Wreturn type and -Wimplicit-fallthrough infractions in the IR interpreter. Moreover, default switch cases on enum classes are removed to leverage compiler complaints of missing cases, which ensures that all related switch logic gets thoughtfully extended when the enums are extended themselves.		2021-11-28 10:29:08 +01:00
..
compiler	chore: update IR interpreter enum hygiene	2021-11-28 10:29:08 +01:00
constructions	feat: basic support for definitions at inductive declarations	2021-10-25 12:44:35 -07:00
annotation.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
annotation.h
aux_recursors.cpp
aux_recursors.h
bin_app.cpp
bin_app.h
class.cpp	chore: remove dead code at Class.lean used by old frontend	2020-11-20 16:51:44 -08:00
class.h	chore: remove dead code at Class.lean used by old frontend	2020-11-20 16:51:44 -08:00
CMakeLists.txt	chore: move pp_options.cpp to Lean	2021-01-27 14:16:12 +01:00
constants.cpp	fix: gen_constants_cpp.py: mark constants as persistent	2020-11-29 18:59:39 +01:00
constants.h	chore: remove unused names	2020-10-27 16:28:19 -07:00
constants.txt	chore: remove unused names	2020-10-27 16:28:19 -07:00
expr_lt.cpp	fix: dllexport functions not already annotated in header	2021-09-20 18:41:46 +02:00
expr_lt.h	chore: remove dead code	2020-10-27 19:23:14 -07:00
expr_pair.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
expr_pair_maps.h
expr_unsigned_map.h
formatter.cpp	chore: remove io_state & abstract_type_context	2021-01-12 09:51:14 -08:00
formatter.h	chore: remove io_state & abstract_type_context	2021-01-12 09:51:14 -08:00
init_module.cpp	chore: move pp_options.cpp to Lean	2021-01-27 14:16:12 +01:00
init_module.h
max_sharing.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
max_sharing.h
module.cpp	fix: dllexport functions not already annotated in header	2021-09-20 18:41:46 +02:00
module.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
num.cpp
num.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
print.cpp	fix: dllexport functions not already annotated in header	2021-09-20 18:41:46 +02:00
print.h	chore: remove io_state & abstract_type_context	2021-01-12 09:51:14 -08:00
profiling.cpp	chore: raise default profiler.threshold to 100ms	2021-08-04 16:40:57 +02:00
profiling.h
projection.cpp	refactor: move is_structure_like to inductive.cpp	2021-11-25 11:31:00 -08:00
projection.h	refactor: move is_structure_like to inductive.cpp	2021-11-25 11:31:00 -08:00
protected.cpp	chore: remove legacy support for modification objects	2020-10-26 08:10:51 -07:00
protected.h
reducible.cpp
reducible.h
replace_visitor.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
replace_visitor.h	chore: remove Expr.localE constructor	2020-11-01 09:37:48 -08:00
sorry.cpp	chore: remove dead code	2020-10-25 20:49:30 -07:00
sorry.h	chore: remove dead code	2020-10-25 20:49:30 -07:00
suffixes.h
time_task.cpp	fix: dllexport functions not already annotated in header	2021-09-20 18:41:46 +02:00
time_task.h	refactor: pos at time_task::time_task was a dead field	2021-01-30 11:10:18 -08:00
trace.cpp	chore: remove C++ messages	2021-01-12 09:51:14 -08:00
trace.h	chore: remove C++ messages	2021-01-12 09:51:14 -08:00
util.cpp	refactor: move is_constructor_app to inductive.cpp	2021-11-25 11:31:00 -08:00
util.h	refactor: move is_constructor_app to inductive.cpp	2021-11-25 11:31:00 -08:00