Ssreflect Users Discussion List

[Assia Mahboubi <>]

Dear Keiko,

   to  my knowledge, this is indeed not possible. The 'set' tactic 
folds the abbreviation in the goal, and you need to rewrite the 
definition explicitly in the context if needed. More generally there is 
no way to provide a "universal" argument to an ssreflect tactical, I 
mean an argument representing "all the  facts in the context".

   I would tend to think that if you define the abbreviation early 
enough in your script, i.e. as soon as the subterm to be captured by the 
definition appears in your goal, the problem should not arise.
But may be I am wrong or may be you are in a situation where this is not 
convenient? In this case I would be happy to see an example if possible.

Hope this helps,

assia


 a écrit :
> Hello again and thank you for the reply yesterday.
>
> Is it possible to define an abbreviation and fold it in all the facts 
> appearing
> in the context without enumerating all their names?
> I could not find out how to do it with set + in tacticals.
>
> Best regards,
> Keiko
>