diff --git a/src/Init/Lean/Elab/StructInst.lean b/src/Init/Lean/Elab/StructInst.lean index 45c3e58b87..eedf81fed7 100644 --- a/src/Init/Lean/Elab/StructInst.lean +++ b/src/Init/Lean/Elab/StructInst.lean @@ -787,6 +787,10 @@ fun stx expectedType? => do | some _, _ => throwError stx ("invalid {...} notation, explicit source is required when using '[] := '") | _, _ => elabStructInstAux stx expectedType? sourceView +@[init] private def regTraceClasses : IO Unit := do +registerTraceClass `Elab.struct; +pure () + end StructInst end Term end Elab