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

fix: missing test

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-06 07:18:27 -07:00
parent 73ee2d92aa
commit d9fcfd71d9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/LCNF/MonoTypes.lean
View file

@ -42,7 +42,7 @@ Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do
if isRuntimeBultinType declName then return none
let .inductInfo info ← getConstInfo declName | return none
if info.isUnsafe then return none
if info.isUnsafe || info.isRec then return none
let [ctorName] := info.ctors | return none
let mask ← getRelevantCtorFields ctorName
let mut result := none