Kenny Lau (Jul 12 2020 at 12:35):
import group_theory.free_group #check free_add_monoid.of open free_add_monoid -- invalid namespace name 'free_add_monoid'
Kevin Buzzard (Jul 12 2020 at 12:55):
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
Kenny Lau (Jul 12 2020 at 13:03):
free_add_monoid is already defined
Rob Lewis (Jul 12 2020 at 14:57):
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
Last updated: May 11 2021 at 22:14 UTC