cannot open namespace free_add_monoid

Stream: general

[Kenny Lau]

import group_theory.free_group

#check free_add_monoid.of

open free_add_monoid -- invalid namespace name 'free_add_monoid'

[Kevin Buzzard]

I've never known the logic for what makes a string of characters a valid namespace. What happens if you define free_add_monoid to be empty?

[Kenny Lau]

free_add_monoid is already defined

[Rob Lewis]

It seems like add_decl is missing a call to some kind of namespace creation trigger.

import tactic

def ns1.hi : ℕ := 3

open ns1

open tactic
run_cmd do add_decl $ mk_definition `ns2.bye [] `(ℕ) `(3)

-- open ns2

def ns2.ok : ℕ := 5

open ns2

#check bye