coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] using a hypothesis
- Date: Thu, 10 Jan 2019 00:24:27 +0000
- Accept-language: en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:C/F4EB1Q3Zbe5Dw5smDT+DRfVm0co7zxezQtwd8ZseMWLPad9pjvdHbS+e9qxAeQG9mDu7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJwgqBUoBO9qBJwzIHZe52VO+Fkc6/BYd8WWWhMU8BMXCJBGIO8aI4PAvIFM+lGtYnyuV4OrBujDgeiHuzuxCRIhnjw3aYn1OkvFR/J3BY+ENILsHXYttv7O70cUOCuy6nIyy7OYOlQ2Tfg8oTHbA0uoeyWUb1qbMrc0E8iHB7LgFWXrIzqJTKV1uIVvmia6epgT+OvhHQ9pwF/uDiiwNonhIrRho8NxV3I6T91zJspKdC6UkJ3fNCpHZpKuyyeK4d6Wt4uTmF0tCog1LEKpZC2cDIUxJg62xLTceGLfoaM7x77WuaePzR1iG5gdb+6hBu+7Uytx+/5W8S73lZFszdJn9zQuX0P2BHe7s2KReV980u9xTmC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBjP7l0vrgqOKa0ko4++m5ev6brn/oZ+TLJF7hhv5MqQzhsywGuM4MhUIX2eG4+i8zKfj/UrlQLpUkvI2jqjZsJfcJcgBoa65HhNV0oIk6xa4DDeqysgXnX4CLF5deRKHiZbmO03WLf33EfuzmUmgnCtpyvzcI7HsDJTAImLHnbv9Zbp97lRTyAs3zdBR/ZJUDbQBLer3VEDvrtzXEBo5Mgyuz+jpEtp82JgeWWWJAqKCKqzSt0KI6vgxLOaReY8ZoizyK+U96/70kXA5gUMdfbWu3ZYPdH+4Ge1mL1yFbnron9cOCnwHvhE+TezvkF2NSyRfZ3e0X6Im5zE0EpiqDYnZRtPlvLvUliy8B9hdYn1MIlGKC3bhMYueEb9YYyWLZ8RljzYsVL67SoZn2wv45yHgzL8yDOfO9ygJ/b7qy8Ny4aWHtxwo+DllSeiUzHqKSUl9mH5OSjMrmqli9x8ugmyf2LR11qQLXedY4OlEB19jZMzsitdiAtW3YTrvO9KASVKoWNKjWGtjR9QshdICfgB0Bof710yR72+RG7YQ0oezKtks6KuFhSr4Ids7xnrbkqA83QF/H5l/cFa+j6s6zDD9Qo7El0LFyPSDSJ9EhWvo2T7GymCD+kZFTAR3TKPJG2gFYVfbpsj44UWESKKyDbMgMU1KzsvQc6Y=
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
Hi all,
thanks for all the replies, all seem helpful, but I'm trying to analyse
what they are doing, with the help fo the documentation.
At
https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacv.specialize
it lists
Variant specialize (ident term*) as intro_pattern
with the word ident in bold black type.
Elsewhere bold black type seems to indicate sutff which should be typed
in literally, but here it looks as though this isn't so.
Is this an error in the documentation?
Cheers,
Jeremy
- [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, Pierre Courtieu, 01/10/2019
- Re: [Coq-Club] using a hypothesis, Jeremy Dawson, 01/10/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
- Re: [Coq-Club] using a hypothesis, Li-yao Xia, 01/08/2019
Archive powered by MHonArc 2.6.18.