Improve notation
Make prettier notation for the SolveSep
, BiAbd
, IntroduceHyp
, IntroVars
constructs. These should resemble their semantics, so that goals containing them are still somewhat readable. It should additionally fix the need to explicitly state the TT
arguments. Also for ReductionStep!
Some ideas:
-
P ∗ [R] ⊲ [M] Q ∗ [S]
.. but what about variable bindings? -
SolveSep constructs -
BiAbd & Abd -
ReductionStep'
Edited by Ike Mulder