coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] using a hypothesis

From: Lily Chung <ikdc AT mit.edu>
To: <coq-club AT inria.fr>
Subject: Re: [Coq-Club] using a hypothesis
Date: Tue, 8 Jan 2019 01:49:03 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=Pass smtp.helo=postmaster AT NAM02-BL2-obe.outbound.protection.outlook.com
Importance: Normal
Ironport-phdr: 9a23:Jk3kWhCT7IxMY8oPNbMeUyQJP3N1i/DPJgcQr6AfoPdwSPv9osbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJOSM3/mLVhcJwkqxUowivqB1wzIHIb4+YL/p+cbjHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5eoYn8o1sPrQa1CBesBOPyzD9IiWL90Ko70+QiDA7JwBctH9cPsHTIttn6KrodUf2swaTO0D7NYfRW2TLn54jJdBAsuf6MXbNsccrR1EkgDBnJgUmXqYzgOT6ey+cDs3CD4udvSe6jkXMrpx1zrzS1xMohipPFip8Lxl3H7Sl13YU4Kce2RUJne9KoDYVcuiOAO4drTM4uX2dlszsgxLIco560Zi0KxYwnxxHBb/yHdJCF7Ar/WeiWPTt0mmtpda+5iRqs6ESgzfbzWdeu3FZNsypFjsLDtncQ1xzV98eLUON9/l2m2TaTyQ/c9v1EIUEzlardMZIhxaMwloYXsUTEGS/2m1/6g7ORdkUh4uSo6uLnbav6ppKEOIJ4lhvyPrkylsG9G+g1MAgDU3KG9eii17Dv5Uj5T69Ljv0ynKnZqpfaJcEDq664AA9az5os5g26DzenzNQUh2cII09YeB6flYjmJ0nOIOzkDfe4m1mjjDBrx+nfMrL9BpXNM2PMnaz6fbd97k5c0BA8wcpe55JSELEBIej8VlX/tNzCXVcFNFngyOH+Td55y4k2WGSVA6bfPrmE4nGS4ed6B+iIdcc+uCv7JLBx5v3ihlc8mENbcKW0i8hEIEukF+hrdh3KKUHnhc0MRD9T71gOCdfygVjHagZ9InO7XqYy/DY+WdCjDJuFS4yw0uXYgHWLW6ZOb2UDMWiiVG/yftTWXvYQLi+eP505y2FWZf2aU4YkkCqWmkr6xr5gcrWG3AQ97cim/vwvourZmFc16CB+CNmb3yeVVWZok2gURjgwmqdivUh6zVTF2q990aVV
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

I have two custom tactics I use for exactly this purpose.

https://gist.github.com/ichung/032b849da0c3c5e3987c83f835d111ee

[Coq-Club] using a hypothesis, Jeremy Dawson, 01/08/2019
- Re: [Coq-Club] using a hypothesis, Li-yao Xia, 01/08/2019
  - Re: [Coq-Club] using a hypothesis, Jeremy Dawson, 01/10/2019
    - Re: [Coq-Club] using a hypothesis, Pierre Courtieu, 01/10/2019
      - Re: [Coq-Club] using a hypothesis, Théo Zimmermann, 01/11/2019
- Re: [Coq-Club] using a hypothesis, Lily Chung, 01/08/2019
- Re: [Coq-Club] using a hypothesis, Marko Doko, 01/08/2019
  - Re: [Coq-Club] using a hypothesis, Théo Zimmermann, 01/08/2019