Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 150
    • Issues 150
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 11
    • Merge requests 11
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #73
Closed
Open
Created Mar 05, 2017 by Robbert Krebbers@robbertkrebbersMaintainer

Specialization patterns syntax extensions

There have been some requests to add new stuff to specialization patterns:

  1. A // token for performing done. One could then write things like [$H1 $H2 //] or [//].
  2. Being able to frame in persistent specialization patterns, i.e. [# $H1 $H2].
  3. A token, say [$] to solve the goal by framing, and by keeping all unused hypotheses for the subsequent goals.

However, there are some questions here:

  1. I suppose we want to be able to use // also for pure and persistent goals. For example [% //] and [# //].
  2. What is going to happen when we do [# H1 $H2]. There are some obvious choices: a.) using a hypothesis without a $ prefix is forbidden b.) ignore all hypotheses that are not prefixed with a $ (there is no need to select hypotheses, you get all anyway, since the goal is persistent) c.) prune the context that goal.
  3. What to frame? Just the spatial hypotheses, or everything (including the persistent ones)?

Anyone some ideas? I would like to have a syntax that is not too FUBARed.

Assignee
Assign to
Time tracking