coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [HELP] All branches of `match` yield same value

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] [HELP] All branches of `match` yield same value
Date: Tue, 16 Jan 2018 19:52:34 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
Ironport-phdr: 9a23:Y65hwhRPA/KUVVNC3ftgedYomNpsv+yvbD5Q0YIujvd0So/mwa69YxGN2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mLKhMJwkqxVrhCupxJjzIDTb46YL/V+cr/HcN4AX2dNQsRcWipcCY28dYsPCO8BMP5coYn6vVQBsRu+BQipBOjy1zJInGH53awm0+QnDw7GxhErEtULsHvOrdX1MLwfUeKyzKbS0TrDb/JW2TLk5IfTaBAuv/CMXa52ccXP00kjDR7KgUuJpIHjIjib2OMNs22B4OphU+Kik2wnqwZrrTezxscsi4zJipsOxVDe6yp5wZo1JdumR05he9KrDYVfuieHPIV1WsMvW3xktSQ7x7EcvZO3ZjYGxIkpyhLFdvCKfYaF7xT+X+iLOzh4nmhqeLenihay70egzur8W9G00FlUtCpFl8fDtmsX2xzI9MeHUOV98Vm72TmV0gDc8PtILl0qmqbDKp4hxKA/loYLvEjeHCL7mV/6gauMekk65+Sl5f7rbqjoq5KSL4N0jxvxMqUqmsyxG+Q4NQ0OUnCe+eum1b3j+Vb0QLdNjvIsjqbZsJHaJcECqqGiGQ9azIcj6wq5Dzi4ytQUh2QII0xddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd9V14UEWGvJDLXKHrnVtAqq4eskI+iJLKUPtTfhLfU/r6rrhH49sV0adKKp3J5SYmq1H+hgLl/fbXe60YRJKnsDogdrFL+is1aFSzMGPy/jDZJ53SkyDcedNamGQ4mshLKb2yLhR89UYWlNClGJVH3yeoSYXfoWLi6fcJU4zm40EIO5Qopk7imA8RfgwuA+fOjT8yYYtJem3sJ45vHVmAt0+TEmV53AgVHIdHl9myYzfxFz3K17phYkmFeOy611mLpDGMZN6ulAVw58OZOOl+E=

Hi,

Am Dienstag, den 16.01.2018, 16:28 -0800 schrieb Ramkumar Ramachandra:
> What tactic can I use to collapse all the cases?

the pedestrian way that I know and would do is

destruct r; destruct body; reflexivity.

(but I am curious if something better will be mentioned here).

Joachim

--
Joachim “nomeata” Breitner

mail AT joachim-breitner.de
https://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] [HELP] All branches of `match` yield same value, Ramkumar Ramachandra, 01/17/2018
- Re: [Coq-Club] [HELP] All branches of `match` yield same value, Joachim Breitner, 01/17/2018
- Re: [Coq-Club] [HELP] All branches of `match` yield same value, Heiko Becker, 01/17/2018
  - Re: [Coq-Club] [HELP] All branches of `match` yield same value, Merlin Göttlinger, 01/17/2018