coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] any Ltac2 examples out there?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Tej Chajed <tchajed AT mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] any Ltac2 examples out there?
Date: Wed, 22 Apr 2020 13:00:02 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f176.google.com
Ironport-phdr: 9a23:oxmibRywaCQyTznXCy+O+j09IxM/srCxBDY+r6Qd2uoWIJqq85mqBkHD//Il1AaPAdyGra4bwLuG+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhIiTanbr5/Lhq6oAHSu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8rxmQwH0higZKzE58XnXis1ug6JdvBKhvAF0z4rNbI2IKPZyYqbRcNUHTmRDQ8lRTTRMDI28YYUREuQPPuRXr4f6qVQBsRSwChKhBP/txzJSmnP7x7E23/onHArb3AIgBdUOsHHModn7NqcSVua1zKjLzTrda/NZxyny5ZPHchAku/6MXLZwfdDNxkkoEgPJgEibpIvnPzOS0OQNsmub4PRkVe2xlWEqsA5xoj21ycctjonFnJ4aylfB9Shgxos+ONO2SEl+YdG+EZtQsTmXN4R3QsM+Q2FopT01xqcatp68eSgHzoksyR3Ha/GfbYSE/hbuWPySLDp4nn5pZqyziwio/US9yODxV9G43EhLoyZZj9XBs20B2hjP5cWCRfZw/1ut1SqK2g/O6uxLO0U5mrfYJpE63LE9k5Uevl/NHi/4nUj2grGZe0Q69eWt7+nofqvqqYKaOoRpkA/xKL4ulda6AekgMggBQWyb+eOk2b3m50L5QbFKguQvkqnarZzWPMobqrO7DgJUyIoj5BG/DzCp0NQcg3YLNk5KeBWCj4TxOlHOJu73DeunjliyjDtmw+rKM77hD5nXMHTPjqntcaxg50NeyQc/1dVf6IhVCrEFLvLzQEjxtNnAAx87NAy0xefnCNZj2YMaR22AHLSUMKzXsVCS5+IvJ/OAa5MSuDb4M/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1YCM3m+QHpRUa2wOXkyHEX7qeomsXvYQLi+eP5kyvCYDUO3rSYgn1BKjsAL347ViJ+vQvCYfsNirgNpy4ezQmBU/+BR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6UtxqUATYUPtcMMaR8zMNvn98I/E8r7A1uTcdKASVLgSdKjU2loE4ABhuQWakM4IO2MyxDO2y3wXe0Qnr2PQYU3q+fShievYcl6zHnC2e8qiFx0GpIeZ13jvbZ28k3oP6CMlkyYk6iwcqFFhXzC8W6CySyFu0QKCQM=

Thanks for these links, Tej!

On Wed, 22 Apr 2020 09:23:01 -0500
Tej Chajed
<tchajed AT mit.edu>
wrote:

> I've written an Ltac2 tutorial
> <https://github.com/tchajed/ltac2-tutorial> with a handful of
> examples and detailed explanations. I also have a repo for Ltac2
> experiments <https://github.com/tchajed/coq-ltac2-experiments> with
> slightly bigger examples but less documentation.
>
> I haven't really used the backtracking support, although it looks
> cool; I'd recommend reading user-contrib/Ltac2/Pattern.v in the Coq
> sources to see how `match! goal with` and `match! constr:(...) with`
> are implemented, which is based on the Control.plus, Control.case,
> and Control.zero primitives.

[Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Jason Gross, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Tej Chajed, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
  - [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] Ltac2 retraction bug?, Maximilian Wuttke, 04/22/2020
      - Re: [Coq-Club] Ltac2 retraction bug?, Pierre Courtieu, 04/23/2020
        
        Re: [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/23/2020