max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove two workarounds

Browse source 
They are not needed anymore after 83775b08cb
This commit is contained in:
Leonardo de Moura 2021-02-05 15:21:57 -08:00
parent b6d7d9569e
commit eb510c16c3
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -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