coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] folding under binders

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] folding under binders
Date: Mon, 24 Sep 2018 20:41:37 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f171.google.com
Ironport-phdr: 9a23:H1NMqRb0oVpkJDJPVcrDEVH/LSx+4OfEezUN459isYplN5qZoMW9bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE28G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYpcUAOoBPOZYtIn9qEUNrRCjGQSsAvngyjlViXTr2qA1yf8uEQHH3Aw7H9IBrnfUoM/vO6cUS++1yrTHwS/Cb/NXxTf955PFch8kof6WXLJwddDdxlUoFwPAl1idr5HuMT2S1uQIqWeb7uxgWPqzhG4gsQFxpCagxsMoioXTmI0a103E+CNky4g2Pd21UFB3bcKgHZdKtCyXN5F6Tt0/T2xsoio2178LtYO9cSMX0poo3QTfZOaCc4WQ4hLsSuKRITBgiXJgYr2/hhKy/VGgy+LnS8W4yVhKojdHn9XRrHwN2BvT6s+ISvt54EitwyqA1wfW6u1cIEA0k7TUK4I5z7IuipYetV7PEyz2lUnskqOaa0Ep9vK15+nlf7nqvpqcOJV1igH6PKQugMu/AeEgPwcURGeb+eW81Kbj/ULnQ7VGlOc5kq/Dv5DcOMsXvK+5Aw5J0oYs8Bu/ADKm384ZnXkDNl5KZBWHj43xN1HUPP/4Feu/g0irkDpz2//GOaThDozRIXjHjbfuZq1w61VcyQo21dBQ/YhYCrAHIPLpW0/+rsbUDhEjM1/8/+GyA9Jkk4gaRGjHVqSeKebZtUKCzuMpOeiFIoEP7mXTMf8gstfkjX4imVIeNYCv1J0bICSxFPRnOEWUYjzlhN4HHSELvxYxZOPvgVyGFzVUYiDhDOoH+jgnBdf+Xs/4TYe3jenZhXbpLthtfmlDT2u0PzLtfoSAVe0LbXvLcMBkmz0AE7OmTt14jE38hErB07Nia9Hs1GgAr5u6jYp64uTSkVc58jkmV53AgVHIdHl9myYzfxFz3K17phYjmFKK0Kw9kvYBUNIKuKoPXQA9OprRied9DoKqVw==

Is there a convenient way to fold a definition under binders?

(I can do a `change` of the whole term, but that is problematic when dealing with large terms)

Consider the following example:

Definition add2 n := n +2.

Goal (fun n => n) = (fun n => n+2).

Is there a general advanced fold tactic such that `advanced_fold add2` changes "n+2" to "add2 n"?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] folding under binders, Abhishek Anand, 09/25/2018
- Re: [Coq-Club] folding under binders, Clément Pit-Claudel, 09/25/2018
  - Re: [Coq-Club] folding under binders, Hugo Herbelin, 09/25/2018