LemmaDoc / NewLemma with Namespaces

[Trequetrum]

I'm not sure if this is a bug or if it's a documentation issue. When I do the following, I get an error in File 2 despite being able to use foo_bar within my level's statement. Getting rid of the namespace does fix the problem.

File 1, define and document a theorem:

namespace Sumfin
def foo_bar(h : α) : α := h
LemmaDoc foo_bar as "foo_bar" in "∩" "TODO"

File 2, part of a level:

open Sumfin
NewLemma foo_bar -- ERROR: unknown identifier 'foo_bar'
Statement (P : Prop) : P → P := foo_bar -- No Error

[joneugster]

That's a documentation issue, updated it. NewLemma, LemmaDoc and all these are supposed to take a fully-qualified name as first argument.

I.e. LemmaDoc Sumfin.foo_var and NewLemma Sumfin.foobar would be the expected syntax.

(I suppose nowadays we could change this behaviour to actually take namespaces into account, we might not be at a point anymore where this is necessary. But that would need to be an active decision, with some work behind it.)

[Trequetrum]

I've got it working :)

Working on taking namespaces into account doesn't feel necessary (Or at least doesn't feel like it needs to be a priority of any sort). It might make sense to consider a simpler feature regarding how text is generated for theorem info-pages. For example, NNG4 only has a single namespace MyNat, and users are never required to enter it explicitly. Therefore:

four_eq_succ_three

MyNat.four_eq_succ_three : 4 = MyNat.succ 3

really could be streamlined:

four_eq_succ_three : 4 = succ 3

This has the added benefit of not requiring the game to teach users about namespaces unless otherwise necessary.

[joneugster]

Indeed, that's been logged as #128 and should really be addressed at some point