alias ignores private

Stream: general

[Yaël Dillies]

I wasn't expecting the following #checks to work.

import tactic.alias

section

private alias nat.add_le_add_iff_right ↔ foo bar
private alias nat.lt_of_add_lt_add_left ← baz

end

#check foo -- foo : ?M_2 + ?M_1 ≤ ?M_3 + ?M_1 → ?M_2 ≤ ?M_3
#check bar -- bar : ?M_2 ≤ ?M_3 → ?M_2 + ?M_1 ≤ ?M_3 + ?M_1
#check baz -- baz : ?M_1 + ?M_2 < ?M_1 + ?M_3 → ?M_2 < ?M_3

[Yaël Dillies]

I am willing to fix this myself, but I don't know how private works. Is it an attribute? Can alias detect it has been tagged?

[Yaël Dillies]

Context is #16141

[Mario Carneiro]

It's passed along to the command in the decl_meta_info. User commands can choose to not take that argument, in which case they don't support any modifiers (private, protected, noncomputable, @[attr] and /-- doc comment -/ are all in there)

[Mario Carneiro]

but if they do take the argument then they can potentially have any of those and can do what they want with it

[Yaël Dillies]

Ah so alias takes it and ignores it?

[Mario Carneiro]

then again, the capabilities of lean 3 meta code to apply this information to other commands is limited

[Mario Carneiro]

yeah, it doesn't seem like there is any way to do the equivalent of creating a private def from meta code. I'm going to say this is out of scope for the lean 3 version (it's already been ported to lean 4 so you can do it there). It wouldn't be too hard to check the decl_meta_info and give an error if you put weird modifiers on the declaration though

[Yaël Dillies]

Does alias actually do anything with any attribute? If not, we could remove its decl_meta_info altogether

[Mario Carneiro]

it uses the doc string

[Yaël Dillies]

Hmm, doesn't it autogenerate the docstring, actually?

[Mario Carneiro]

yes, unless you put a doc string on the alias command

[Kyle Miller]

Lean 3 core usually throws errors when there are unexpected modifiers. (Sometimes this leads to usability bugs, for instance you used to be able to write /-- foo -/ @[class] noncomputable local infix ` + ` := nat.add even though the infix command only looked at local.)

[Kyle Miller]

If it doesn't already exist, it might be good to have a standard function to call to check that certain modifiers are not set and report a standard error message if they are. For example, here's one source in the C++.