Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Retain branch information in match for holes.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Retain branch information in match for holes.


Chronological Thread 
    < Chronological >      < Thread >
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Retain branch information in match for holes.
  • Date: Sat, 14 Aug 2021 10:17:41 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
  • Ironport-hdrordr: A9a23:3+bVDanrl/12GuZevBp+KQN0BO/pDfI73DAbv31ZSRFFG/Fw5Pre+MjztCWE7Qr5N0tApTntAsa9qDbnhPxICOoqTNSftWvd1ldARbsKheDfKn/bdxEWndQ26U4PScVD4ZHLbWRHsQ==
  • Ironport-phdr: A9a23:iNtpIRQ6vyIlJxlvWceBnN/7T9psommfAWYlg6HPa5pwe6iut67vIFbYra00ygOTBcOLtLkZ16L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNfwlEnjmwbLF9IBi2ogjaq9Ubj5ZlJqst0BXCv2FGe/5RxWNmJFKTmwjz68Kt95N98Cpepuws+ddYXar1Y6o3Q7pYDC87M28u/83kqQPDTQqU6XQCVGgdjwdFDBLE7BH+WZfxrzf6u+9g0ySUIcH6UbY5Uimk4qx2ShHnlT0HOiYk/m/JhMx+jKFVrhyvqBNwwYHbfJqYO+Bicq7HZ94WWWRMU8RXWidcAo28dYwPD+8ZMOtEsobyvV4OpgagCAmsAOPvyydIiWXy3aIgzu8sFhvJ0xE6ENILrHvZt8n6NLwIXuC0yKnE1zDDb/JK2Tvn9ofHbw0hrOiKULltfsXf1VMhGBnZjlWMt4PlJTWV2/wMvmaV8+dsSOyihm0lpgxwoDWj29khhpfUiowbxV3I6SV0zoY0KNC7SEN1YcOpHZpMuy+VKYZ6X98vTn11tCg6zLANpJC1fC8PyJs9xh7fbeSKfJSI4hLnVeaROS13hHZ/d76lgRa971Sgx+vhXce3yFZHtjdJnsfPu3wX2RHf9tKLRuVn8ku/xDqDyxjf5+NKLEwui6bXNposzqQxm5cTq0jPAzH6lFnwgaSLbEsr4PKo5P7iYrj+pp+TKYt0igbmP6Qph8y/Hes4Mg8PX2id9uSwzabj/VHjT7VWlPI6iLXWsIvAKsQaoq61GQpV0oc/6xqlETipzckYkWEGLFJDZh2Hk5DkN0zQLP37F/uyjUignC11y/zcILHtH4nBImDGkLj7fLZ970BcyBA0zdBa/59bEKwOL+j2WkDtr9HXEgQ5PBa1w+bjEtl904IeWX6VDqCHLazSrEeE5vgzLOmUeI8VpDH9JuA56P7plH81gEMSfa203ZQMc324BfRnI0CBYXX2mNsBEGEKvhA/TOPwklGCXyRTND6OWPc34Sh+A4a7B6/CQJqsifqPxnSVBJpTM0lKA1XEOnfsdp2NX/5EPCueK8pqujcfXLmlDYogyVejuBKsmOkvFfbd5iBN7cGr79Ny/eCGzXnaGhR/FM2c1yeITn0yk28VFWZeNEFXplFhxVCC16c9mOBRCdUV7OhAUwN8MJ/AieF2FoKqMuokVtySQVeiBNCnHXc8Qs9jm7cz
On 8/14/21 9:14 AM, Suneel Sarswat wrote:
I am looking for a more general anwer, i.e., how to carry branch information during the proof.
In general, books and tutorials are probably better than mailing lists to get general answers.  I do think mine Certified Programming with Dependent Types should clear this up and share general principles.  Though it's probably helpful to read from the start, you'll start seeing your particular issue addressed around Chapter 8.

Archive powered by MHonArc 2.6.19+.

Top of Page