Zulip Chat Archive

Stream: general

Topic: weird simp behavior


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?

Yury G. Kudryashov (Apr 11 2020 at 15:59):

Probably type of something depends on the old H.

Kevin Buzzard (Apr 11 2020 at 16:03):

Is the old H mentioned in eg the goal?


Last updated: Dec 20 2023 at 11:08 UTC