From 677561522db50ceef216ff0edf36db442953370d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 1 Dec 2025 12:02:03 +0100 Subject: [PATCH] fix: add missing import (#11441) This PR fixes an issue that prevented the manual from building due to the missing explanation of an error. --- src/Lean/ErrorExplanations.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/ErrorExplanations.lean b/src/Lean/ErrorExplanations.lean index 422b78b4f8..11883115bc 100644 --- a/src/Lean/ErrorExplanations.lean +++ b/src/Lean/ErrorExplanations.lean @@ -8,6 +8,7 @@ module prelude public import Lean.ErrorExplanations.CtorResultingTypeMismatch public import Lean.ErrorExplanations.DependsOnNoncomputable +public import Lean.ErrorExplanations.InductionWithNoAlts public import Lean.ErrorExplanations.InductiveParamMismatch public import Lean.ErrorExplanations.InductiveParamMissing public import Lean.ErrorExplanations.InferBinderTypeFailed