Zulip Chat Archive

Stream: general

Topic: conv is slow


Kenny Lau (May 19 2020 at 07:16):

import data.complex.exponential

set_option profiler true

-- elaboration of test took 5.55s
lemma test (x : ) : real.cos (x + x) * 0 = real.cos x * 0 :=
begin
  conv in (real.cos x) {}
end

Mario Carneiro (May 19 2020 at 07:16):

irreducible all the things?

Kenny Lau (May 19 2020 at 07:17):

does irreducible solve everything?

Gabriel Ebner (May 19 2020 at 07:26):

It should become faster when you finish the proof. conv implicitly does refl at the end.

Gabriel Ebner (May 19 2020 at 07:28):

Also, which mathlib version are you using? It's quite a bit faster for me:

elaboration of test took 22.1ms


Last updated: Dec 20 2023 at 11:08 UTC