Naive question about unknown-var test case

[nobodxbodon]

In unknown-var.aya:

def Nat : Type | zero
def p => Nat::suc Nat::zero

Checking it outputs as expected below:

Error: The qualified name Nat::suc is not defined in the current scope

Question is, after I remove Nat::suc, it still gives similar error about Nat::zero:

Error: The qualified name Nat::zero is not defined in the current scope

In module-basic.aya, it seems ::zero works. So why not in unknown-var.aya?

[ice1000]

Did you mean data Nat?

In module-basic.aya, it seems ::zero works.

Because they did open data Nat instead of data Nat. The keyword open brings Nat::* into the current scope. You can think of it as using namespace in C++.

[ice1000]

I think the point of unknown-var.aya is to test the error message of an unknown qualified name, and that's why there's no suc defined -- we are using an undefined variable, and we expect an error message about unknown qualified name.

Anyways, why are you learning from some wrong code? I found it very interesting while quite confusing.

[nobodxbodon]

I wanted to see what errors can be found, so I started from operator/ambiguous.aya in failure folder. Then I wanted to try Chinese identifiers, so I tried in unknown-var first and then rec-adt.aya (glad to see renaming negs to 负 works).

I'm a bit surprised that you're surprised :) I find the test cases for errors are at least as interesting as the functional ones.

I think the point of unknown-var.aya is to test the error message of an unknown qualified name, and that's why there's no suc defined -- we are using an undefined variable, and we expect an error message about unknown qualified name.

For this purpose, can unknown-var.aya be simplified to below?

def Nat : Type
def p => Nat::suc

[nobodxbodon]

Saw your fix. Looks good.

[ice1000]

We even support emoji identifiers. But I don't think it's a good idea. This might be changed.

[ice1000]

I don't know. I don't have a persuasive argument.