Allow using qualified symbols from the current module

Consider the following program:

module example;

axiom A : Type;
inductive T (A : Type) {
c : A -> T A;
};

end;

Inside the constructor c the first occurrence of A is a reference to the type parameter. To check out this, run the scoper:

$ juvix scope example.juvix --show-name-ids
module example@0;
  axiom A@1 : Type;

  inductive T@3 (A@2 : Type) {
    c@4 : A@2 → T@3 A@2;
  };
end;

At the moment, there is no way to refer to A@1, i.e., the axiom A. I'd expect to be able to write a program like the following.

module example;

axiom A : Type;
inductive T (A : Type) {
c : example.A -> T A;
};

end;

$ juvix microjuvix typecheck example.juvix
/home/jonaprieto/example.juvix:5:5-14: error:
Qualified symbol not in scope: example.A

I don't think this qualifies as a bug. I would argue that this is the desirable behaviour

That's true. I thought I pressed the feature request button. The labels are part of the issue template.

Navigation Menu