coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] how to instantiate existential variables
- Date: Mon, 3 Dec 2018 23:51:00 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f45.google.com
- Ironport-phdr: 9a23:7ShI8xLvQWOkcFPIDtmcpTZWNBhigK39O0sv0rFitYgQI/nxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhygJNzE78G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYY8VAOoaOuZYqZT2qVoUrRu5HgmsH/7kxzhKhnDsxq061OIhEQ7c3AwnBNIOq3DZoc76NKcXS++1za3IwS/fYPNR3Dfw8Y7FeQ0ir/GURb98b9bdxE01Gw7Gjlics5LpMy+W2+gXvGWW7+xtXv+1hWE9sQF+uD2vy98siobXgoIVzUjJ9SBjz4Y0Id20UVB0bsO5HJdJuSGXOIt7TtktQ2FvvyY6xbkGtoChcCcWz5QnwgbTa/2Bc4eW/hLuTPidLSt8iX5/e7+yhwy+/Va8xuD/TMW531ZHojJAktbWt3AN0xLT6tKASvt45kqh2yyA1xvU6uFCLkA0j63bK4U6wrM0jZcTvkHDETX3mEXylqOZakIk+u2w5+T9frrmvoOcN5NzigzmLqsundW/Df0kPQgKQmiU4v+x1Kbj/E38WLVFlOc6kqjfsJDAJMQUvLS1AwFP0tVr1xHqBDC/ld8cgHMvLVRfeRvBgZK6FUvJJaXaBOy4hRyDijBw3LiSPLT6BZPCNH/Yi+bJcrN06koaww02m4MMr6lIA60MdaqgEnT6s8bVW0dgYl6Eht3/AdA47bswHGeGA6uXKqTX6Aba6ecmIu3Kb4gQ6m+kd6oVosX2hHp8omczOLGz1MJOOn+9F/ViZU6eZCi024pTISIxpgM7CdfSphiCXDpUPSvgWqs94nQ2BNvjA9ueAI+qh7OF0WGwGZgEPm0=
You can instantiate them by number
instantiate (4 := B). instantiate (2 := A). This is not very satisfying, but it works.
On Mon, Dec 3, 2018, 23:07 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:
Hi,
thanks for all the answers to my previous question.
FWIW, actually simpl seems to rewrite a goal without instantiating evars
Another question about evars:
given a goal
Γ1 ++ l ++ A :: Γ2 ++ B :: Γ3 = ?Γ1 ++ ?A :: ?Γ2 ++ ?B :: ?Γ3
how do I instantiate ?A to A and ?B to B?
I've tried
instantiate (?A := A).
and
instantiate (A := A).
but both those produce error messages.
thanks
Jeremy
- [Coq-Club] how to instantiate existential variables, Jeremy Dawson, 12/04/2018
- Re: [Coq-Club] how to instantiate existential variables, Jason Gross, 12/04/2018
- Re: [Coq-Club] how to instantiate existential variables, Théo Zimmermann, 12/04/2018
- Re: [Coq-Club] how to instantiate existential variables, Jean-Christophe Léchenet, 12/04/2018
- Re: [Coq-Club] how to instantiate existential variables, Jason Gross, 12/04/2018
Archive powered by MHonArc 2.6.18.