sneeuwballen/zipperposition

infix syntax doesn't work

medovina opened this issue · 2 comments

medovina commented

I've been experimenting with the induction examples in examples/ind. The function definitions in nat.zf include an attribute "infix", which seems to imply that infix syntax should work:

def[infix "+"] plus : nat -> nat -> nat where
  forall (X:nat). ((plus z X) = X);
  forall (X:nat). (forall (Y:nat). ((plus (s X) Y) = (s (plus X Y)))).

So I tried modifying nat1.zf to use infix syntax for addition:

include "nat.zf".
goal
  forall (X:nat).
    (forall (Y:nat).
       (forall (Z:nat). X + (Y + Z) = (X + Y) + Z )).

Unfortunately with this change Zipperposition fails to find a proof, even though it can easily prove the original version of nat1.zf.

Is the infix syntax known to be broken? It would be nice to be able to use it.

c-cube commented

Hi! The infix notation is only used for printing, I'm afraid. The parser is pretty simple and only knows of a predefined, fixed set of infix operators (+ will be on int/real, not on custom types). Printing operators nicely is still useful when you comb through lots of debug logs :).

medovina commented

Aha - I see. OK - I agree that even if it's only for printing, it's still nice to have. :)

  • 👍1