one.foo : Nat
one.foo = 18
bar : Nat
bar = foo + foo
Here, we expect `foo` to resolve to the `one.foo` in the file, because although it could also refer to `two.foo` in the namespace, that wouldn't type check.
Yet the transcript fails, and with a confusing/wrong error message, too:
Loading changes detected in scratch.u.
I couldn't figure out what foo refers to here:
5 | bar = foo + foo
The name foo is ambiguous. Its type should be: Nat
I found some terms in scope that have matching names and
types. Maybe you meant one of these:
This transcript shows odd behavior:
Loading changes detected in scratch.u.
I couldn't figure out what foo refers to here:
The name foo is ambiguous. Its type should be: Nat
I found some terms in scope that have matching names and types. Maybe you meant one of these:
one.foo : Nat one.foo : Nat