Zulip Chat Archive

Stream: general

Topic: weird simp behavior


view this post on Zulip Sebastien Gouezel (Apr 11 2020 at 15:41):

In my context, I have

H :
  k, blocks_fun 
    finset.sigma (finset.range N) (λ (n : ), fintype.pi_finset (λ (i : fin n), finset.Ico 1 N))

Then I do simp at H and I get in the context

H :
  k, blocks_fun 
    finset.sigma (finset.range N) (λ (n : ), fintype.pi_finset (λ (i : fin n), finset.Ico 1 N)),
H : k < N   (a : fin k), 1  blocks_fun a  blocks_fun a < N

So, the first H hasn't disappeared, but a new one with the simplified version has appeared. No MWE, sorry. Any idea why this could happen?

view this post on Zulip Yury G. Kudryashov (Apr 11 2020 at 15:59):

Probably type of something depends on the old H.

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 16:03):

Is the old H mentioned in eg the goal?


Last updated: May 14 2021 at 07:19 UTC