Specialization patterns syntax extensions
There have been some requests to add new stuff to specialization patterns:
//token for performing
done. One could then write things like
[$H1 $H2 //]or
- Being able to frame in persistent specialization patterns, i.e.
[# $H1 $H2].
- 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:
- I suppose we want to be able to use
//also for pure and persistent goals. For example
- 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.
- 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.