Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Hello,

The syntax you are looking for is "rewrite -/blah"

Note that this tactic is more powerful than the standard tactic "fold",
notably as it can handle placeholders. For example,
  "rewrite -/(not _)"
will succeed if there's one negation in the goal that can be folded, while
  "fold (not _)"
will raise "Error: Cannot infer this placeholder."

Best,

Erik

On 09/21/2013 02:16 PM, t x wrote:
> With apologies for a stupid question -- I've searched through
> http://hal.inria.fr/docs/00/40/77/78/PDF/RT-367.pdf
>
> I know that "unfold blah" = "rewrite /blah"
>
> However, what does "fold blah" map to in "rewrite" ?
>
> Thanks!

--
Érik Martin-Dorel
Post-doctorant, Équipe-projet Marelle
Inria Sophia Antipolis - Méditerranée
http://erik.martin-dorel.org/