coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to rewrite, needed to match goal

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to rewrite, needed to match goal
Date: Tue, 29 Dec 2020 22:47:13 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f182.google.com
Ironport-phdr: 9a23:9QaISxeM0EK3IRGWgzxjJTrvlGMj4u6mDksu8pMizoh2WeGdxcS/YR7h7PlgxGXEQZ/co6odzbaP7Oa6AzZLvMnJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRe7oR/PusUIn4duJaY8xxnUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vugJxw4DUbo+WOvRxcKzSctEGSmRORctRSy5MD5mgY4cTAecMP+BVpJT9qVsUqhu+ABGhCf3ryjhSg3/5w6s60/g5Hg/c3QwgA8sCvWrQrNrvKacdTP66zK3VxjjEc/xWwTb96JTUfRAlu/6MQK9/ftTVyUQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyhGEptxt/rSKzxscwlIbJnIQVx0jY+Sh9zog7K8C0RU90bNOnDJZdqy6XOpd2T84hTG9lpSY0x7wCtJKmfCUH1ogqyhHfZvGFd4WF/BHuWumQLDp8gn9uZbGxhw6q/ES+1uHxUtO43VVKoyZfjNXAqG4B2wbO5sWEVPdx5lmt1DmV2w3S9+1IO144mKXHJ5I7wbM8ipweulnZECDsgkX5lqqWe10k+ue27+TnZa3rppqGOI91jgHyK70ums+iDeghPAgCQmuW9fqm2L3s+k35R7pKjvkonaXDrJ/aIsEbqra4Aw9TzIkj9w6yAym63Nkch3UKL1JIdAiZg4T3JV3COu30APShj1i0lTdk3fHGPrnvApXXKXjDla/scqpl605d1Ao80dRf6IhJCr4cPv3zXlT8tNPdDhAjMgy0x/zrB8l61oMbQW6PGLOWMLvOsV+U4eIiO/WDZIgMuDrkN/cl4+PugmQilF8Gfaip2IMXZ2qiEvRnJUWZe3vsjc0bHWcEpAptBNDt3VaFSHtYY2u4d6M6/DAyToy8XqnZQYX4q7gA2Sq9AqpuZ3wDIVSFDHvlc83QUO8NdCmWK9JtnzgsWr2oSotn3har4lypg4F7J/bZr3VL/ano08J4srWKyEMCsAdsBsHY6FmjCmF5mmRSGW0z1aF75FV+kxKNiPgixfNfEtNX6rVCVQJobceNndw/MMj7X0f6RvnMTV+nRtu8BjRoF4A+xtYPZwB2HNDw10mfjRrvOKcckvmwPLJx6rjVhiGjKMN0ynKA364k3QEr

On 12/28/20 8:10 AM, Jeremy Dawson wrote:
> I'm presuming this is because the existential ?l0 is expected to have type
> involving lpst. Is there a way of getting Coq to show the type of an
> existential?

You can use `Show Existentials.`; it will give you the type of ?l0 (and the
hypotheses available in its context)

[Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
  - Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/17/2020
    - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
    - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/28/2020
      - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
      - Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020