| .. |
|
borrowed_annotation.cpp
|
chore: remove dead code
|
2020-10-28 09:33:19 -07:00 |
|
borrowed_annotation.h
|
feat: elaborated borrowed annotations
|
2020-10-16 15:17:58 -07:00 |
|
closed_term_cache.cpp
|
chore: remove legacy support for modification objects
|
2020-10-26 08:10:51 -07:00 |
|
closed_term_cache.h
|
|
|
|
CMakeLists.txt
|
|
|
|
compiler.cpp
|
fix: do not invoke add_extern for declarations marked with implementedBy
|
2022-01-14 20:27:50 -08:00 |
|
compiler.h
|
|
|
|
cse.cpp
|
chore: reduce src/include/lean
|
2021-09-07 08:24:54 -07:00 |
|
cse.h
|
|
|
|
csimp.cpp
|
fix: add workarounds to code generator
|
2022-02-25 08:47:56 -08:00 |
|
csimp.h
|
|
|
|
eager_lambda_lifting.cpp
|
refactor: move is_constructor_app to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
eager_lambda_lifting.h
|
|
|
|
elim_dead_let.cpp
|
chore: remove Expr.localE constructor
|
2020-11-01 09:37:48 -08:00 |
|
elim_dead_let.h
|
|
|
|
erase_irrelevant.cpp
|
fix: skip value if type is computationally irrelevant
|
2022-02-17 10:41:16 -08:00 |
|
erase_irrelevant.h
|
|
|
|
export_attribute.cpp
|
|
|
|
export_attribute.h
|
|
|
|
extern_attribute.cpp
|
fix: do not invoke add_extern for declarations marked with implementedBy
|
2022-01-14 20:27:50 -08:00 |
|
extern_attribute.h
|
fix: do not invoke add_extern for declarations marked with implementedBy
|
2022-01-14 20:27:50 -08:00 |
|
extract_closed.cpp
|
refactor: move is_constructor_app to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
extract_closed.h
|
|
|
|
find_jp.cpp
|
|
|
|
find_jp.h
|
|
|
|
implemented_by_attribute.cpp
|
|
|
|
implemented_by_attribute.h
|
feat: skip code generation for declarations marked with implementedBy, init, and builtinInit
|
2022-01-14 19:20:16 -08:00 |
|
init_attribute.cpp
|
chore: reduce src/include/lean
|
2021-09-07 08:24:54 -07:00 |
|
init_attribute.h
|
|
|
|
init_module.cpp
|
|
|
|
init_module.h
|
|
|
|
ir.cpp
|
chore: missing trace_pp_expr
|
2022-02-17 10:40:21 -08:00 |
|
ir.h
|
|
|
|
ir_interpreter.cpp
|
feat: allow interpretation of constants initialized by native code
|
2022-03-07 10:59:49 +01:00 |
|
ir_interpreter.h
|
chore: reduce src/include/lean
|
2021-09-07 08:24:54 -07:00 |
|
lambda_lifting.cpp
|
refactor: move is_constructor_app to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
lambda_lifting.h
|
|
|
|
lcnf.cpp
|
chore: reduce src/include/lean
|
2021-09-07 08:24:54 -07:00 |
|
lcnf.h
|
|
|
|
ll_infer_type.cpp
|
refactor: move is_constructor_app to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
ll_infer_type.h
|
|
|
|
llnf.cpp
|
refactor: move is_constructor_app to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
llnf.h
|
|
|
|
reduce_arity.cpp
|
|
|
|
reduce_arity.h
|
|
|
|
simp_app_args.cpp
|
perf: add temporary hack for performance issue
|
2020-10-15 13:37:29 -07:00 |
|
simp_app_args.h
|
|
|
|
specialize.cpp
|
feat: mark arguments such as {_ : BEq α} as specialization target
|
2022-01-17 13:05:50 -08:00 |
|
specialize.h
|
|
|
|
struct_cases_on.cpp
|
refactor: move is_constructor_app to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
struct_cases_on.h
|
|
|
|
util.cpp
|
fix: missing test at has_trivial_structure
|
2022-03-25 17:36:30 -07:00 |
|
util.h
|
fix: make sure Quot primitives stay in eta expanded form
|
2021-10-08 09:36:06 -07:00 |
