coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tactic Notation wrapper for ssreflect rewrite

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Tactic Notation wrapper for ssreflect rewrite
Date: Mon, 1 Jan 2018 12:51:03 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:dpa/jBYRrtv/TeTYyejHDef/LSx+4OfEezUN459isYplN5qZoMW/bnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAn8G/Zl89+gqxVrx2uuxNxzJXZYJ2XOfdkYq/RYd0XSGhHU81MVyJBGIS8b44XAuQdOuZXtJLyqEUUrRuiGAKiAfnvxSFTiXDtw6I6yf8hGhzB0QwlBd0OsXDUrNTzNKcdVeC1zbLIzSnYb/5Nwzf975PHfQs/rvGWQbJwctDRxlc0GAzekFqQs5flMymT1uQJqmWW6fdrW+G3i2M/tg18rCWjyt0xhoTLiY8Z0E3I+CRjzIooKtC1RlZ3bNqrHZdKqS2WK497TtkgTmxsoio21KAKtJq9cSMX0poo3QTfZOaCc4WQ4hLsSuKRITBgiXJ+fbK/mw6y/VW6xu3nSsa00UhFrixZndbSrHwNzQHT5tKBSvt55kuh2DCP2B7P6uxcPEw5m7fXJ4Q8zrMymZcfq1nPEy7slEnrg6KbeF0o+u2y5OTmZrXmqIWcN4hxigzmN6QhgM2/AeA5MggIUGib/eW81Kb//U3iW7hKlPo2nbLCv5/EP8Qbuq25AxVL3Yk48BmwES2m0M8CkXkBKFJJYAiHgJTxO1HSPPD4Cu+yjEirkDdy3vzJIrnhAojWIXXYi7fgfbN961ZGxwYpzNBf4YhUCrAbL/7pVE/xro+QMhhsOAuthu3jFd81gogZQCeEBrKTGKLUq16BoOw1dbqifogQ7Qz6IfIo/eKmrmU0k1UQZ7LhiZ4eaXS5GPtiIl6FelL2hd0LHH0WvRAzRubnkkbEVzoFNCX6ZL41+jxuUNHuNozEXI342LE=

Hi Coq-club,

I am trying to do something like:

Tactic Notation "foo" ssrrewriteargs(args) :=
do stuff;
rewrite args.

So that for args I can take anything that the ssreflect rewrite tactic accepts, e.g. `lem1 /= lem2 /const //`.

Does anyone know if this is possible and what I should pick for `ssrrewriteargs`?

Thanks!

Robbert

[Coq-Club] Tactic Notation wrapper for ssreflect rewrite, Robbert Krebbers, 01/01/2018
- Re: [Coq-Club] Tactic Notation wrapper for ssreflect rewrite, Robbert Krebbers, 01/08/2018