elpi icon indicating copy to clipboard operation
elpi copied to clipboard

Declaring a predicate `prop` in a namespace causes a typecheck failure

Open pi8027 opened this issue 2 years ago • 1 comments

Example:

From elpi Require Import elpi.

Elpi Command test.
Elpi Accumulate lp:{{

namespace ns {

pred pred1.

pred prop.

}

pred pred2.
pred2 :- ns.pred1.

}}.
Fail Elpi Typecheck.

Declaring pred prop in namespace ns seems to have the effect of changing the return type of the other predicates in the namespace, i.e., pred1, to ns.prop. It results in the following error message.

The command has indeed failed with message:
At least one of the following errors holds: 
File "(stdin)", line 12, column 0, character 58: ns.pred1 has type ns.prop but is used with type prop
File "(stdin)", line 12, column 0, character 58: ns.pred1 has type ns.prop but is used with type goal-ctx

pi8027 avatar Sep 04 '23 09:09 pi8027

oops ;-) prop should be a keyword (hence not usable for a predicate name).

gares avatar Sep 04 '23 11:09 gares