Zulip Chat Archive

Stream: general

Topic: conv is slow


view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 19 2020 at 07:16):

irreducible all the things?

view this post on Zulip Kenny Lau (May 19 2020 at 07:17):

does irreducible solve everything?

view this post on Zulip Gabriel Ebner (May 19 2020 at 07:26):

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

view this post on Zulip 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: May 14 2021 at 04:22 UTC