Sebastian Ullrich 4939f447a3 test: avoid testing colliding private inductives (#11041) ... `prelude-injectivity.lean` was testing inj thm generation for all inductives in core, including private ones, which could lead to name clashes that should not be able to occur in actual files. Put it under the module system to not load private decls in the first place.		2025-11-01 11:47:52 +00:00
..
bin
cmake	chore: fix spelling errors (#10042)	2025-08-22 07:23:12 +00:00
include/lean	fix: revert the waitAny refactoring (#11000)	2025-10-29 08:27:16 +00:00
Init	feat: finish? produces finish only suggestion (#11034)	2025-10-31 14:47:24 +00:00
initialize	feat: zero cost BaseIO (#10625)	2025-10-22 10:55:12 +02:00
kernel	perf: mark move constructors and assignment operators as noexcept (#10784)	2025-10-22 14:21:51 +00:00
lake	refactor: use String.ofList and String.toList for String <-> List Char conversion (#11017)	2025-10-31 14:41:23 +00:00
Lean	test: avoid testing colliding private inductives (#11041)	2025-11-01 11:47:52 +00:00
library	perf: used hashmaps for symbol lookup in the interpreter (#10927)	2025-10-23 11:45:20 +00:00
runtime	fix: revert the waitAny refactoring (#11000)	2025-10-29 08:27:16 +00:00
shell	refactor: lake: mv tests/examples to top-level tests dir (#10688)	2025-10-06 21:47:57 +00:00
Std	fix: Rename theorems that use sorted instead of pairwise (#10743)	2025-10-30 16:07:35 +00:00
util	chore: fix C++ warning (#10922)	2025-10-24 11:09:08 +00:00
cadical.mk
CMakeLists.txt	chore: begin development cycle for v4.26 (#10884)	2025-10-21 23:22:58 +00:00
config.h.in
githash.h.in
Init.lean	chore: more reorganization of strings (#10928)	2025-10-23 11:56:11 +00:00
lakefile.toml.in	feat: USE_LAKE_CACHE CMake option (#10708)	2025-10-08 08:56:53 +00:00
lean-toolchain
Lean.lean	chore: use 'library suggestions' rather than 'premise selection' (#11029)	2025-10-31 04:07:49 +00:00
lean.mk.in	chore: further split libleanshared on Windows to avoid symbol limit (#10136)	2025-08-26 16:01:57 +00:00
Leanc.lean	fix: Unicode path support for Lean Windows executables (#10133)	2025-08-27 11:28:55 +00:00
out	feat: ac normalization in grind (#10146)	2025-08-27 03:28:30 +00:00
Std.lean	chore: more module system fixes and refinements for finishing batteries port (#10819)	2025-10-21 08:19:50 +00:00
stdlib.make.in	chore: further split libleanshared on Windows to avoid symbol limit (#10136)	2025-08-26 16:01:57 +00:00
stdlib_flags.h	chore: remove comment from src/stdlib_flags.h (#10409)	2025-09-16 10:39:27 +00:00
version.h.in