## Stream: general

### Topic: 1

#### Kenny Lau (Jul 05 2019 at 14:35):

example (H : (2:ℤ) = (1:ℤ)) : true :=
by change _ = 1 at H; trivial --fails

example (H : (2:ℤ) = (1:ℤ)) : true :=
by change _ = @has_one.one _ _ at H; trivial -- works


#### Kenny Lau (Jul 05 2019 at 14:36):

how strongly is 1 associated with nat?

#### Kevin Buzzard (Jul 05 2019 at 14:36):

change is quite happy to fail if it decides what your input means and then realises that it's nothing to do with what the hypothesis it's supposed to be changing is.

#### Kevin Buzzard (Jul 05 2019 at 14:37):

When I see change fail I sometimes change change X at H to def Z := X

#### Kevin Buzzard (Jul 05 2019 at 14:38):

and often the def fails. If the def fails I think change just fails. I don't think change looks at what it's supposed to be changing until it's made the thing it's supposed to be changing it to. That's my impression at least.

#### Kevin Buzzard (Jul 05 2019 at 14:38):

So in the first case I guess change is trying to solve the metavariables ASAP, without looking at H, and so it solves them using nat.

#### Mario Carneiro (Jul 05 2019 at 14:41):

That is nat defaulting you are seeing. If a numeral doesn't have a particular type after elaboration it defaults to nat

#### Mario Carneiro (Jul 05 2019 at 14:41):

I think the change expression might be elaborated separately from the goal to cause this behavior

Last updated: May 13 2021 at 23:16 UTC