coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] cutrewrite

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] cutrewrite
Date: Sat, 18 Jul 2020 10:11:08 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f42.google.com
Ironport-phdr: 9a23:bOvdqhEpM3bJjqZD4Uoo5p1GYnF86YWxBRYc798ds5kLTJ7zp8WwAkXT6L1XgUPTWs2DsrQY0rSQ6PCrADZaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmsowjctcYajZZ8Jqov1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2hqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4TwuVsOrQG/BQm3GejhxCVHhnrt3aYn1OkuDQHG3BYhH9IVqnjbsc/6NKIJUeyvyqnIyS7Ob/xT2Tjn6YjIdgotru2LXbJ1aMfcz1QkGAzZgFuKs4PlIy+V2foXs2id9+dtWv6jhW4opQ9/vzSixtkhh4rXiowbzl3I6yp3zYY6KNClS0N2YdCpHIVMuiybOIV7QM0sT39mtion17ALt561cS4Xw5ok3x7Sc+KLf5SM7x75V+ucIS10iGx4dL6jnRq//lasx+vhXceuyllKtDBKktzUu3ANyRPT7s+HR+N4/ki72DaP0xnf6uZYIUwpjKbbJZEszqAqmpoctkTDGSD2mEHog6OMakok/e2o5/zmYrXguJCcK5d5hh/iPqkqgMCyAuQ1PhIQU2SG5eiwzrLu8VPhTLVPlPI2k63ZsJ7AJcQco660GxNa0oY56xa+FDeqyskXkmMCLFJeYh6HiYzpNkrBIPD9F/i/glCsnC13yPDBO73tGo/NIWTbkLf9YbZ97FZRxxY0zdBG/p5bFrUBIO/oVULqr9zZDho5MxSuzOr9CdV90JkeWWOVDaODPqPSqwzA2uV6KO6VIYQRpTy1f/Mi/rvliWIzsV4bZ6igm5UNPiOWBPNjdm6Ze3v3yvsIFHxC6gE+Vu3xzlGLVCUVYXKaUKc15zV9A4WjW9SQDruxiaCMiX/oVqZdYXpLXwjVQCXYMr6cUvJJUxq8Z8pokzgKT7+kEtZz2hSntQu8wL1ifLONp38o8Kn73d0w3NX90BE/8TsuUpaY2mCJCmZoxyYGG2Vw06d4rkhwjFyE1Pog2qAKJZlo//pMFzwCG9vE1eUjUoL9XwvAepGCT1P0Gtg=

Dear all,

Coqide says that cutrewrite is deprecated. The docs say that I should use the enough tactic instead. So I can do 'enough (a = b) as ->' instead of 'cutrewrite (a = b)'. This works but what do I do when I would want to do 'cutrewrite (a = b) in H'. I.e., use cutrewrite to rewrite something in a hypothesis?

Regards,

Chris

[Coq-Club] cutrewrite, Chris Dams, 07/18/2020
- Re: [Coq-Club] cutrewrite, Laurent Thery, 07/18/2020
  - Re: [Coq-Club] cutrewrite, Chris Dams, 07/20/2020
    - Re: [Coq-Club] cutrewrite, Théo Zimmermann, 07/20/2020
- Re: [Coq-Club] cutrewrite, Fabian Kunze, 07/20/2020