Skip to content

GitLab

Closed
Created by Ike Mulder@snyke7Maintainer3 of 3 tasks completed3/3 tasks

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