Feature Request: Prefix equality

[Durbatuluk1701]

The problem

I am working with a tool that synthesizes/extracts code into CakeML. Unfortunately, this tool does not provide the ability to infix its equality check (=?) during extraction and could only extract prefix operators. Thus my extracting a s1 =? s2 function yields = s1 s2, which, insofar as I have tested, is rejected by the CakeML compiler.

I have a workaround where I can instead extract equality checks to (fn x => fn y => x = y). This allows for compiling working extracted code, but makes maintaining the code more difficult as readability is greatly reduced.

Possible Solutions

1. Is there possibly a way to get prefix equality in CakeML that I just have not found yet?
2. In the CakeML standard library, Double.= exists and if a similar operator were added for Char, String, etc. that would be viable for my purposes
3. Modifying the = operator (or adding another similar one) that can be performed in a prefix fashion
4. I can get over it because optimally I should not need to be reading my verified extracted code anyways

Let me know if you need any more info from me. I would be happy to help develop any of these solutions, although it may take me a while to get up to speed on the repository to complete it.

[tanyongkiam]

For solution 1: the way to write prefix equality is op= (similar to SML)

Edit: to be clear, what I mean is CakeML already supports solution 1, try writing op= s1 s2 instead in your example.

[Durbatuluk1701]

Perfect, exactly what I need. Thank you @tanyongkiam