export?

Stream: general

[Kevin Buzzard]

From lean core:

[Kevin Buzzard]

class has_pow (α : Type u) (β : Type v) :=
(pow : α → β → α)

export has_andthen (andthen)
export has_pow (pow)

[Kevin Buzzard]

What does export do? The line reminds me of those old batman TV shows.

[Kenny Lau]

like open

[Kevin Buzzard]

oh I just remembered #help

[Kevin Buzzard]

export: create aliases for declarations

[Kevin Buzzard]

At the end of the day, does this just mean that pow can be used instead of has_pow.pow?

[Kevin Buzzard]

Aah -- does it mean that this is true globally?

[Kevin Buzzard]

I see -- #check pow seems to work fine in a new file

[Kevin Buzzard]

so it's open on steroids

[Kevin Buzzard]

"open and never close"?

[Johan Commelin]

No, I guess that is an artifact of the fact that it is in core.

[Johan Commelin]

Hmm, no... that is not what I meant.

[Sebastian Ullrich]

"open and never close"?

Yes, basically. You can locally "close" it with hide.

[Kevin Buzzard]

Thanks Sebastian.

[Kevin Buzzard]

The reason I asked was that I noticed that if I import tactic.ring then I can do a ^ 2 for a in a comm_ring, but I can't do this otherwise. I was just trying to figure out where that instance was defined, but I don't know how to do this, short of looking at what tactic.ring imports and importing all of those things instead, until I finally find the import which actually makes it work.

[Kevin Buzzard]

That's one approach -- and searching for has_pow.pow is another, but actually I should just search for pow perhaps

[Kevin Buzzard]

Got it -- obviously to get powers in a ring the key import is group_power.lean ;-)

[Kevin Buzzard]

[mumble mumble monoid]