pow/mul associativity

Stream: general

[Reid Barton]

What's going on here?
image.png

[Bolton Bailey]

docs#pow_mul

[Bolton Bailey]

I'm not seeing anything amiss, do you find something surprising about this lemma?

[Yakov Pechersky]

That the LHS should look like a ^ (m * n), otherwise it looks like (a ^ m) * n.

[Bolton Bailey]

It seems like the parentheses are there in the code, I guess the doc-gen just removes them?

[Reid Barton]

docgen uses the pretty printer I think. But Lean itself displays the lemma correctly for me (if I just import the file that contains this lemma). Maybe there is some other notation elsewhere that confuses it?

[Yury G. Kudryashov]

What if you import all.lean?

[Eric Wieser]

What's the precedence of pow and *?

[Kevin Buzzard]

Just to remark that pow is right associative and mul left associative

[Eric Wieser]

#print notation ^  -- _ `^`:80 _:79 := has_pow.pow #1 #0
#print notation *  -- _ `*`:70 _:70 := has_mul.mul #1 #

[Eric Wieser]

Except, after doc-gen runs open_all_locales to agressively turn on notation, it becomes

#print notation *  -- _ `*`:9001 _:70 := has_mul.mul #1 #0

[Eric Wieser]

Which is the fault of this line

[Gabriel Ebner]

Feel free to submit a PR to ignore this notation (we already have a long list of ignored localized notation).

[Eric Wieser]

Do we want to ignore that notation though, for files about parsers?

[Gabriel Ebner]

We can only ignore notations globally in doc-gen, so we don't really have a choice there.

[Eric Wieser]

Do you mean that in a "that was the easiest thing to implement" way, or "there is no lean core API that would allow us to do anything different"?

[Gabriel Ebner]

In both ways, yes. Right now we generate all documentation in the same tactic call (with the same open locales). Maybe we can now open locales programmatically (using run_parser), but it would be a bit of refactoring.