Zulip Chat Archive

Stream: general

Topic: cannot open namespace free_add_monoid


view this post on Zulip 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'

view this post on Zulip 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 empty?

view this post on Zulip Kenny Lau (Jul 12 2020 at 13:03):

free_add_monoid is already defined

view this post on Zulip 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