Alethe specification on arguments of an anchor unclear
Arguments of an anchor can for example look like this:
(anchor :step t57 :args ((veriT_vr26 Loc) (veriT_vr27 Loc) (:= y veriT_vr26) (:= x veriT_vr27)))
- There used to be an assumption that if there is a (variable, sort) tuple (
(veriT_vr26 Loc)
) for a variable (veriT_vr26) and an mapping(:= y veriT_vr26)
for that same variable that then the mapping has to occur after the (variable, sort) tuple. Since the context is a list it seems fine to restrict the order (Section 2 of the Spec).
Talking to @hjsc it seems like this should still be the case but it is not in the Standard yet. If this should be a restriction could it be added please?
- Additionally the Standard define e.g., the bind rule:
Here it seems like the bind rule needs a context that first lists a number of variables and then a number of mappings. However, during previous discussion with @hbarbosa and @hjsc I learnt that they can be in a different order.
- In section 2 it says on subproofs:
"To indicate these changes to the context, every anchor is associated with a list of fixed variables and mappings. This list can be empty."
However, the grammar allows anchor steps without this list. Either the word "every" should be deleted here or the grammar should be adapted