Skip to content

Make Hoare triple tex macro compatible with e.g. array environment

The \hoare macro in the iris.sty tex file is quite incompatible with the array environment (likely, among other things). An example is seen as follows:

Screenshot_2022-05-13_at_16.53.25

That is, adding a top alignment [t] to the environment causes odd newline behaviour.

The proposed change fixes this problem, as seen as follows:

Screenshot_2022-05-13_at_16.52.34

It is the impression that the change is conservative.

NB: In general, it is my impression that the iris.sty file is used quite widely, and could maybe use some community-driven improvements. Among other things, I have experienced some hiccups including, but not limited to:

  • Incompatibility with existing standards, such as LMCS's template (where the \prop macro is reserved)
  • Missing standard macros (such as \bool and \integer types)

It might be worthwhile discussing whether a higher level of curation could be a benefit to the community.

Edited by Jonas Kastberg

Merge request reports