Zulip Chat Archive

Stream: general

Topic: 1


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

view this post on Zulip Kenny Lau (Jul 05 2019 at 14:36):

how strongly is 1 associated with nat?

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

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 14:37):

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

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

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

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

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