dot notation in namespaces

Stream: general

[suiluj]

Hello,
i have a few different approaches to function of a type. So i wanted to put them into different namespaces, but realized because the function now isn't directly under the type i can no longer use the syntactic sugar where i don't need to write the type, when calling the function on a value.
Is there any way to achieve a short notation here? Or could this behavior perhaps be changed as long as the namespace is open?
Thank you in advance for you time and answers.

namespace N

def Nat.foo: Nat → Nat := id
#eval (1).foo
-- Error no Nat.foo only N.Nat.foo
#eval N.Nat.foo 0

end N

def Nat.foo: Nat → Nat := id
#eval (1).foo

[Aaron Liu]

You can export it

[suiluj]

Thank you for your answer.
I wasn't able to produce the answer i want with export. (It shortly worked but it just was a bug, that didn't work after restarting the file).
I want to be able to use the shortcut inside of the namespace but self exports don't seem to be possible and even outside i can get Nat.foo to be defined but it still has the type N.Nat.foo and therefore the . notation doesn't work.

namespace N
open N -- doesn't seem to make a difference
export N (Nat.foo) -- invalid 'export', self export

def Nat.foo: Nat → Nat := id
#eval (1).foo
-- Error no Nat.foo only N.Nat.foo
#eval N.Nat.foo 0

end N

export N (Nat.foo)
#check Nat.foo -- N.Nat.foo
#eval (1).foo
-- invalid field notation, function 'N.Nat.foo' does not have argument with type (N.Nat ...) that can be used, it must be explicit or implicit with a unique name

[Notification Bot]

suiluj has marked this topic as resolved.

[Notification Bot]

suiluj has marked this topic as unresolved.

[Jon Eugster]

There are also the options to use section N instead of namespace N or to add _root_. to the theorem name like def _root_.Nat.foo which will name the theorem Nat.foo. Just in case you're not aware of them.

Do you want your statement to be duplicated as N.Nat.foo AND Nat.foo or just the latter?

[suiluj]

Thank you for your answer. My goal is code like this, with different definitions of the helper function Nat.foo in different Namespaces.

namespace N

def Nat.foo: Nat → Nat := id
def val := (1).foo

end N


namespace M

def Nat.foo: Nat → Nat := id
def val := (1).foo

end M

[suiluj]

My current solution is to just use different names, but i feel like using namespaces or something similar would make it cleaner and reduce the risk of typing errors.

def Nat.fooN: Nat → Nat := id
def valN := (1).fooN

def Nat.fooM: Nat → Nat := id
def valM := (1).fooM