Zulip Chat Archive
Stream: lean4
Topic: assign slow
Reid Barton (Jun 06 2023 at 15:41):
Should this be possible? What is involved in Meta.isDefEq.assign?
[Meta.isDefEq.assign] [7.784801s] ✅ ?p := [...]
Sebastian Ullrich (Jun 06 2023 at 15:50):
Are there no child nodes? Is this with trace.profiler?
Reid Barton (Jun 06 2023 at 15:50):
It was, yeah
Reid Barton (Jun 06 2023 at 15:50):
No displayed child nodes
Reid Barton (Jun 06 2023 at 15:52):
The parent node was solving some refl p =?= (x = x) problem and all the time was spent in this node
Reid Barton (Jun 06 2023 at 15:52):
Inside simp inside aesop_cat, I think
Mario Carneiro (Jun 06 2023 at 15:58):
the only expensive thing I can think of in assign is the occurs-check
Last updated: Dec 20 2023 at 11:08 UTC