We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 41bc534 commit bc76286Copy full SHA for bc76286
src/Lean/Meta/Match/MatchEqs.lean
@@ -229,7 +229,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
229
assert! matchInfo.altInfos == splitterAltInfos
230
-- This match statement does not need a splitter, we can use itself for that.
231
-- (We still have to generate a declaration to satisfy the realizable constant)
232
- addAndCompile <| Declaration.defnDecl {
+ addAndCompile (logCompileErrors := false) <| Declaration.defnDecl {
233
name := splitterName
234
levelParams := constInfo.levelParams
235
type := constInfo.type
0 commit comments