Sebastian Ullrich ebd22c96ee fix: mark failed compilations as noncomputable (#12625) ... This PR ensures that failure in initial compilation marks the relevant definitions as `noncomputable`, inside and outside `noncomputable section`, so that follow-up errors/noncomputable markings are detected in initial compilation as well instead of somewhere down the pipeline. This may require additional `noncomputable` markers on definitions that depend on definitions inside `noncomputable section` but accidentally passed the new computability check. Reported at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Cryptic.20error.20message.20in.20new.20lean.20toolchain.3F.		2026-02-23 09:18:21 +00:00
..
Basic.lean	fix: mark failed compilations as noncomputable (#12625)	2026-02-23 09:18:21 +00:00
Basic2.lean	fix: import-merging theorems under the module system (#10556)	2025-09-26 13:02:51 +00:00
ConflictingImported.lean	fix: import-merging theorems under the module system (#10556)	2025-09-26 13:02:51 +00:00
Imported.lean	chore: do not rely on Name.lt for ordering fvars in acLt (#12306)	2026-02-08 14:25:31 +00:00
ImportedAll.lean	fix: no defeq equations for irreducible definitions (#12429)	2026-02-11 11:49:10 +00:00
ImportedAllImportedAll.lean	fix: privacy checks and import all (#10550)	2025-09-26 13:26:10 +00:00
ImportedAllPrivateImported.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
ImportedImportedAll.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
ImportedPrivateImported.lean	chore: even more module system fixes and refinements from Mathlib porting (#10726)	2025-10-15 14:59:09 +00:00
MetaImported.lean	fix: mark failed compilations as noncomputable (#12625)	2026-02-23 09:18:21 +00:00
NonModule.lean	fix: no defeq equations for irreducible definitions (#12429)	2026-02-11 11:49:10 +00:00
PrivateImported.lean	fix: [local simp] on privately imported theorem (#12287)	2026-02-03 12:57:23 +00:00