lean4-htt/src/library
Leonardo de Moura 7b5f283507 chore: remove Expr.localE constructor
It was used by the old frontend
2020-11-01 09:37:48 -08:00
..
compiler chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
constructions chore: remove dead code 2020-10-28 09:33:19 -07:00
abstract_type_context.cpp chore: remove dead code 2020-10-28 09:33:19 -07:00
abstract_type_context.h chore: remove dead code 2020-10-28 09:33:19 -07:00
annotation.cpp chore: remove dead code 2020-10-28 09:33:19 -07:00
annotation.h feat(library,frontends/lean): use mdata instead of hacky cache for position information in preterms 2018-09-02 18:08:41 -07:00
aux_recursors.cpp chore: use aux recursor extension implemented in Lean 2019-11-02 11:48:02 -07:00
aux_recursors.h chore: use aux recursor extension implemented in Lean 2019-11-02 11:48:02 -07:00
bin_app.cpp
bin_app.h
class.cpp fix: mark Lean objects in C++ globals reachable from the new frontend as persistent 2020-10-11 17:43:28 +02:00
class.h chore(library/class): simplify 2019-06-26 16:51:36 -07:00
CMakeLists.txt chore: remove dead code 2020-10-28 09:33:19 -07:00
constants.cpp chore: remove unused names 2020-10-27 16:28:19 -07: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 chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
expr_lt.h chore: remove dead code 2020-10-27 19:23:14 -07:00
expr_pair.h chore: fix includes 2020-05-22 14:17:25 -07:00
expr_pair_maps.h
expr_unsigned_map.h refactor(kernel/expr): implement expr using runtime/object 2018-06-21 16:05:33 -07:00
ext_exception.h chore: fix includes 2020-05-22 14:17:25 -07:00
formatter.cpp fix: mark Lean objects in C++ globals reachable from the new frontend as persistent 2020-10-11 17:43:28 +02:00
formatter.h chore: remove dead code 2020-10-28 09:33:19 -07:00
init_module.cpp chore: remove dead code 2020-10-28 09:33:19 -07:00
init_module.h
io_state.cpp chore(library/io_state): avoid thread local storage 2018-02-16 12:12:50 -08:00
io_state.h chore: remove dead code 2020-10-28 09:33:19 -07:00
io_state_stream.cpp refactor(util/sexpr/options): options as a Lean object 2019-05-16 14:27:44 -07:00
io_state_stream.h chore: remove dead code 2020-10-28 09:33:19 -07:00
json.cpp chore: remove dead code 2020-10-26 07:58:15 -07:00
json.h chore: remove old frontend support from lean.cpp 2020-10-25 10:16:52 -07:00
max_sharing.cpp chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
max_sharing.h
message_builder.cpp chore: remove dead code 2020-10-28 09:33:19 -07:00
message_builder.h chore: remove dead code 2020-10-28 09:33:19 -07:00
messages.cpp chore: remove dead code 2020-10-28 09:33:19 -07:00
messages.h chore: remove dead code 2020-10-28 09:33:19 -07:00
module.cpp chore: remove legacy support for modification objects 2020-10-26 08:10:51 -07:00
module.h chore: remove legacy support for modification objects 2020-10-26 08:10:51 -07:00
num.cpp chore: improve old pretty printer on numeric literals 2020-01-09 13:48:15 -08:00
num.h chore: fix includes 2020-05-22 14:17:25 -07:00
pp_options.cpp chore: cleanup 2020-10-27 09:37:21 -07:00
pp_options.h refactor(util/sexpr): move options and option_declarations to util 2019-05-16 14:37:24 -07:00
print.cpp chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
print.h refactor(kernel): move formatting stuff out of the kernel 2018-06-07 16:28:54 -07:00
profiling.cpp fix: mark Lean objects in C++ globals reachable from the new frontend as persistent 2020-10-11 17:43:28 +02:00
profiling.h refactor(util/sexpr): move options and option_declarations to util 2019-05-16 14:37:24 -07:00
projection.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
projection.h feat: export helper functions 2020-02-25 13:00:22 -08:00
protected.cpp chore: remove legacy support for modification objects 2020-10-26 08:10:51 -07:00
protected.h feat(library/protected): replace C++ implementation with Lean one 2019-05-14 16:12:56 -07:00
reducible.cpp chore(library/init/lean): export as C functions 2019-08-16 20:15:30 -07:00
reducible.h feat(library/reducible): use new Lean implementation 2019-06-24 15:48:12 -07:00
replace_visitor.cpp chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08: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 refactor(library): add suffixes.h with commonly used suffixes such as brec_on 2019-03-21 15:06:43 -07:00
time_task.cpp feat: make profileit actually usable 2020-10-23 18:34:47 +02:00
time_task.h feat(library/time_task): do not report inclusive times 2018-11-05 17:06:32 +01:00
trace.cpp chore: remove dead code 2020-10-28 09:33:19 -07:00
trace.h chore: remove dead code 2020-10-28 09:33:19 -07:00
util.cpp chore: remove dead code 2020-10-28 09:33:19 -07:00
util.h chore: remove dead code 2020-10-27 19:23:14 -07:00