When selecting variables in the sequent to be highlighted in the source, an inconsistency is observable.
a bound (e. g. by let) variable is sometimes not highlighted in at the same position in sequent (formula) and source.
The first image shows a highlighting selecetion of the variable s in the Term s < |this.seqq|. Yet, in the code the variable s is highlighted at the position of the condition s >= 0.
The second image (with undbound variables) shows the expected behaviour.
When selecting variables in the sequent to be highlighted in the source, an inconsistency is observable. a bound (e. g. by
let
) variable is sometimes not highlighted in at the same position in sequent (formula) and source.The first image shows a highlighting selecetion of the variable
s
in the Terms < |this.seqq|
. Yet, in the code the variable s is highlighted at the position of the conditions >= 0
.The second image (with undbound variables) shows the expected behaviour.
let:
no let: