1

Stream: general

[Kenny Lau]

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]

how strongly is 1 associated with nat?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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