Ssreflect Users Discussion List

[Enrico Tassi <>]

On Fri, Feb 12, 2016 at 02:39:30PM +0100, Ralf Jung wrote:
> Hi all,
> 
> We are formalizing a shallow embedding of a logic in Coq, and we are
> using scopes such that we can use the same notation for logic-level and
> Coq-level assertions. However, unfortunately, this does not work well
> with the ssreflect rewrite patterns: If, for example, "_ ★ _" is
> registered as notation in a scope delimited by M, I have to write
> 
>   rewrite [(a ★ _)%M]lemma.
> 
> These additional parenthesis get very tedious. Is there any alternative
> available? Or, if not, is there any chance that a syntax like
> 
>   rewrite [a ★ _]lemma%M.
> 
> could be supported?

Hello, it seems reasonable to me.

A little remark: "lemma" can be an arbitrary expression, a term in fact.
It could even be (lemma (c ★ d)).  Would %M also apply to that ★ ?  It
looks like the reasonable thing to do.

On a side note, did you consider other ways to overload ★ ?
I imagine one could guess which ★ you mean by looking at the type of a
for example.  Am I wrong?

Best,
-- 
Enrico Tassi