(disclaimer: I know that the current decision is to ban explicit quantifiers, but I'm recording this issue nonetheless to avoid forgetting about it if we decide the unban them)
What should happen when the same name is quantified several times in the same scope, e.g.:
@forSome :a.
@forAll :a.
:a :b :c.
In EYE, @forAll seems to have a higher priority, regardless of the order in which the quantifiers appear [1, 2].
CWM, on the other hand, is sensitive to the order [1, 2].
I suggest that this should be detected and treated as an error.
(disclaimer: I know that the current decision is to ban explicit quantifiers, but I'm recording this issue nonetheless to avoid forgetting about it if we decide the unban them)
What should happen when the same name is quantified several times in the same scope, e.g.:
In EYE,
@forAllseems to have a higher priority, regardless of the order in which the quantifiers appear [1, 2]. CWM, on the other hand, is sensitive to the order [1, 2].I suggest that this should be detected and treated as an error.
[1] http://ppr.cs.dal.ca:3002/n3/editor/s/9HDOKvL1 [2] http://ppr.cs.dal.ca:3002/n3/editor/s/F5QEke7U