GitLab

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.