IPM/MoSeL nested disjunction syntax
Would it be possible to support the following syntax for nested disjunctions:
iDestruct H as (H|H|H)
? Similarly to the (H1&H2&H3)
syntax for nested separating conjunctions.
Would it be possible to support the following syntax for nested disjunctions:
iDestruct H as (H|H|H)
? Similarly to the (H1&H2&H3)
syntax for nested separating conjunctions.