open-locale nat makes #check output change

Stream: general

[Kevin Buzzard]

import ring_theory.power_series.basic

#check power_series.coeff_mul
-- power_series.coeff_mul : ∀ (n : ℕ) (φ ψ : power_series ?M_1),

open_locale nat

#check power_series.coeff_mul
--power_series.coeff_mul : ∀ (n : ℕ) («φ» ψ : power_series ?M_1),

A random French quote appears. Is this anything to worry about? I'm manipulating power series involving exp so factorials show up (that's why I open_locale nated).

I have no idea how to find out what open_locale nat does, all I know is that it gives me access to the ! notation.

[Eric Wieser]

Searching for in nat finds its notation for src#nat.totient

[Eric Wieser]

Perhaps there's a better way to show everything in a locale though

[Rob Lewis]

Eric Wieser said:

Perhaps there's a better way to show everything in a locale though

The docs suggest run_cmd print_localized_commands [`nat]

[Eric Wieser]

The docs for localized, presumably?

[Eric Wieser]

It might be cool if doc-gen could show those, although I'm not sure where best to show them

[Bryan Gin-ge Chen]

We could have a separate page showing all the locales.

[Eric Wieser]

That's reasonable

[Eric Wieser]

I assume this is a relatively straightforward task of getting print_localized_cmds to output json

[Eric Wieser]

Is there a zulip linkifier for the doc version of src#print_localized_cmds?

[Bryan Gin-ge Chen]

Not sure what you mean... docs#print_localized_commands ?

[Bryan Gin-ge Chen]

Regarding documentation of the different locales, I was about to open a new issue and I found doc-gen#94 by @Floris van Doorn.