Skip to content

Changed HeapLang operator macros to support both parentheses and spaces

Jonas Kastberg requested to merge jihgfee/iris-coq:heaplang-tex-additions into master

The current macro definitions in heaplang.sty favour a syntax style in which function applications use parenthesised arguments, e.g. fn(arg).

Following a discussion on the Iris helpdesk board, it can be argued that both the styles fn(arg) and fn arg have individual merits, and that authors may wish to use either when e.g. defining their BNF syntax. It thus makes sense to update the macros so that they support both (if possible).

An attempt at achieving this is contained in this MR. The idea is that the macros will insert a space , when the given argument is not parenthesised. For use cases with uncurried arguments such as Alloc e1 e2 the user should write \Alloc\expr_1\spac\expr_2.

There are multiple ways of achieving this.

  1. Adopting the \operatorname latex style, which achieves exactly what we want (proposed by @neven)
  2. Using ifthenelse along with xstring to check if the first character of the argument is (

The MR uses solution 1.


Changed \mathop to \operatorname as it does not cause aforementioned unwanted subscript behaviour.

Changed \DeclareMathOperator to \operatorname for consistency, as they unfold to the same thing (according to

Reverted \Ref -> \NewRef change, as it is no longer enforced by \DeclareMathOperator (this should still be done in a separate MR though).

Edited by Jonas Kastberg

Merge request reports