Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • D Diaframe
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 6
    • Issues 6
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Metrics
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Diaframe
  • Issues
  • #6

Closed
Open
Created May 25, 2021 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 Mar 29, 2022 by Ike Mulder
Assignee
Assign to
Time tracking