Specialization patterns syntax extensions
There have been some requests to add new stuff to specialization patterns:
- A
//
token for performingdone
. 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[% //]
and[# //]
. - 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.