Programmatically determining a constant’s "canonical name"?

Stream: new members

[Louis Cabarion]

If I’ve got this right, a single definition can sometimes be referenced by multiple constant names. For example:

• Bool.or and or point to the same definition.
• Lean.Syntax.StrLit and Lean.StrLit point to the same definition.
• «Prop».forall_iff.match_1 and Prop.forall_iff.match_1 point to the same definition.
• _root_.imp_iff_right_iff, Classical.imp_iff_right_iff and imp_iff_right_iff point to the same definition.
• Prefunctor.id and 𝟭q point to the same definition.

How can I, given any name, programmatically obtain the "canonical" (i.e. non-alias) name?

Concretely:

• Input: "or" → Output: "Bool.or"
• Input: "Lean.StrLit" → Output: "Lean.Syntax.StrLit"
• Input: "Prop.forall_iff.match_1" → Output: "«Prop».forall_iff.match_1"
• Input: "_root_.imp_iff_right_iff" or "imp_iff_right_iff" → Output: "Classical.imp_iff_right_iff"
• Input: "𝟭q" → Output: "Prefunctor.id"
• …and so on.

[Louis Cabarion]

This #mwe shows how the different constant names refer to the same definition:

import Mathlib

#check Bool.or
#check or

#check Lean.Syntax.StrLit
#check Lean.StrLit

#check «Prop».forall_iff.match_1
#check Prop.forall_iff.match_1

#check _root_.imp_iff_right_iff
#check Classical.imp_iff_right_iff
#check imp_iff_right_iff

#check Prefunctor.id
#check 𝟭q

[Aaron Liu]

Some notes

• 𝟭q seems to be just notation. It is not a name, and is not processed like a name.
• «Prop».forall_iff.match_1 and Prop.forall_iff.match_1 generate the same name.