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

chore: remove old bootstrapping hack

Browse source
This commit is contained in:
Gabriel Ebner 2022-09-13 15:20:23 +02:00 • committed by Leonardo de Moura
parent fccb60fb69
commit 00793fcdd8
1 changed files with 3 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Elab/Declaration.lean
View file

@ -159,15 +159,9 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
addDocString' ctorName ctorModifiers.docString?
addAuxDeclarationRanges ctorName ctor ctor[2]
return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
let mut computedFields := #[]
let mut classes := #[]
if decl.getNumArgs == 6 then
-- TODO: remove after stage0 update
classes ← getOptDerivingClasses decl[5]
else
computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
classes ← getOptDerivingClasses decl[6]
let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
let classes ← getOptDerivingClasses decl[6]
return {
ref := decl
shortDeclName := name