coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term"

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term"
Date: Mon, 24 Jun 2019 11:44:06 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f48.google.com
Ironport-phdr: 9a23:cKVemhXpBxmZNQQpp2e7upYAusTV8LGtZVwlr6E/grcLSJyIuqrYbBWHt8tkgFKBZ4jH8fUM07OQ7/m6HzVaqs/b4DhCKMUKC0Zcz51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6os1BfFuGZEd/pZyW91O16enAv36sOs8JJ+6ShdtO8t+9NaXanmY6g0SKFTASg7PWwy+MDlrwTIQxGV5nsbXGUWkx5IDBbA4RrnQJr/sTb0u/Rk1iWCMsL4Ub47WTK576d2UxDokzsINyQ48G7MlMN9ir9QrQ+7qBx+x47UZ5yVNOZ7c6jAc94WWXZNU8BMXCFHH4iybZYAD/AZMOlXoYnypVsAoxW9CwexGu3g1iRFiWXq0aAgyektDR3K0Q4mEtkTsHrUttL1NKIKXO6x1qbI1jLDb/VL0jn88ojIdQshoeqRVr93c8re01IvFwTDjlWfs4zlOCiV1v8JvmWA4OpgUPigi28jqw1rvjevwcIsh5DPi4kIxF7E8iB5z5w0Jd2+UEN7bt+kEIdQtyGHLIR6WN8tQ2ZtuCoiy70Gv4K7czYOyJg92hHQdfqKeJWL7BL7TOudPyt0iXZ/dL+8hxu+61asxvH/W8Wu31tHrSxImcTWuH8XzRzc8M2HR+N9/ki/3TaP0Bje6uReLkA1karXMoAuzaMtmpYKv0TOESz7lF/5jK+RcUUk9eyo5Pr9brr6oZ+cMpd4igD4MqswhsyyGfo0PhQKUmSB+umx1Kfv8VPlTLhJlPE7narUvIjfJcsBp665BwFV0pwk6xa6Fzqm0s4XnWIALFJDdxKHlY/pO0rVIP38Fvq/jFGsny1qx/DCJLHuHpLNLn3bnLf7Ybl981JcyBY0zd1H+51UDagBLOvvVU/1qdzXFQQ0Mxe0wubiENVyzJkSWWOJAq+DMaPdq0WE5uw1I7rEWIhAszHkbvMh+vSm2XQ+gBoWebSj9ZoRcnGxWPp8dRa3e33p1/UICmAM9iUkS/fxwAmAWCVUYXmoWLkntxk0DYunCcHIQYX70+/J5zuyApADPjMOMVuLC3q9L9zYCcdJUzqbJ4paqhJBTaKoEtZz2hSntQu8wL1ifLKNq38o8Kn73d0w3NX90BQ79Dh6FcOYijjfQGR9n2dOTDgzjvkm/B5Nj2yb2K09uMR2UNxe4/QTD1U/PJ/YiuF2UpX8BlKHcdCOR1KrBN6hBGNpQw==

It might be a good idea to submit a pull request for Ltac2 notations for the standard eval redexpr in syntaxes, if you can get them to work, a la the notations for cbv, simpl, etc, in https://github.com/coq/coq/blob/d2abcce128c0ba9f62fed66a1bca9c294be0c9c0/user-contrib/Ltac2/Notations.v#L353

On Mon, Jun 24, 2019, 11:41 Jason Gross <jasongross9 AT gmail.com> wrote:

I believe there is no support for custom reduction strategies (Declare Reduction), but all of the built-in ones have configurable Std.eval_* functions in https://github.com/coq/coq/blob/d2abcce128c0ba9f62fed66a1bca9c294be0c9c0/user-contrib/Ltac2/Std.v#L167-L178.

On Mon, Jun 24, 2019, 08:46 Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq Team,

I wonder if Ltac2 has an equivalent of Ltac1’s “eval redexpr in term” construct.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Soegtrop, Michael, 06/24/2019
- Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Jason Gross, 06/24/2019
  - Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Jason Gross, 06/24/2019
  - RE: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Soegtrop, Michael, 06/25/2019
    - Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Jason Gross, 06/25/2019