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
Example:
Declaring
pred prop
innamespace ns
seems to have the effect of changing the return type of the other predicates in the namespace, i.e.,pred1
, tons.prop
. It results in the following error message.