diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 4eca00f272..d5b94e69b0 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -60,13 +60,11 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
     trace[Elab.definition.scc]! "{preDefs.map (·.declName)}"
     if preDefs.size == 1 && isNonRecursive preDefs[0] then
       let preDef := preDefs[0]
-      -- TODO: check why we need `true ==`
-      if true == preDef.modifiers.isNoncomputable then
+      if preDef.modifiers.isNoncomputable then
         addNonRec preDef
       else
         addAndCompileNonRec preDef
-    -- TODO: check why we need `true ==`
-    else if true == preDefs.any (·.modifiers.isUnsafe) then
+    else if preDefs.any (·.modifiers.isUnsafe) then
       addAndCompileUnsafe preDefs
     else if preDefs.any (·.modifiers.isPartial) then
       addAndCompilePartial preDefs