chore: register `Elab.struct trace class

This commit is contained in:
Leonardo de Moura 2020-05-21 16:33:03 -07:00
parent 3d166f6400
commit 7a964ecbea

View file

@ -787,6 +787,10 @@ fun stx expectedType? => do
| some _, _ => throwError stx ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
| _, _ => elabStructInstAux stx expectedType? sourceView
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.struct;
pure ()
end StructInst
end Term
end Elab