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:50:02 -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-qt1-f181.google.com
Ironport-phdr: 9a23:/jZI8RE86VXSoh6/PmkNDZ1GYnF86YWxBRYc798ds5kLTJ7zosmwAkXT6L1XgUPTWs2DsrQY0rWQ6fq6EjFfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsswndqNcajYRiJ6sz1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrg+/qRxxw4DaY4+bO/RxcazfYdwUSnFMXtpSWiFbHo+wc4UCAugHMO1Fr4f9vVwOrR6mCASyAOPo0DpIiWHw3a0my+svCwDG3BA5E98QtHTbtsj1O7oMXuCx0aLFyinMb+tX2Tfh9IfIdgouoeyRUr1udcrc0kYvFwbfgVWRrYzpJS+a1uMIs2WC6edrSO2ghXI9pQ5rvjiv2tkjipPPho8NyV3J8St0zYk3KNO3SkN1bsKpHZlQuiybK4Z7RsEvT39ntSs5yLALuoO2cTUExZg6xxPRZeKKfouK7xzjW+icITF1j29mdrKnnxu+71Ssx+nmWsS30FtGtDdJn9jQunwXyhDe6dWLRuNj8kquwzqC1h3f5vtaLU07iabXMZ0szqI2m5EOq0rMBDX2l1/zjKKOdkUr5Oyo6+P/b7XjvJCcNot0hhjnMqQyh8CzGOo4PhUNUmSG4+i827rj/Ur2QLVOkPI6iLXWsJffJcgDp665BRFa0po75hqhEzur1M4UkHoHIV5fZR6KjpTlN0vTLP37EPuzm1Gsny1qx/DCML3hGJLNLn3bnbj9ZbZ96lJcxxY3zd9F+pJbF68OIPboV0/+sdzXFB45Mwiuz+n7D9V905sSWXiTDa+BLKPSrViI6/ozLOmLfY8ZoSryK/w45/H1lnI5gl8cfayx3ZQNcny4H/JmI1+YYXX2mNsBH30K7UICS7nhj0THWjpObV6zWbg973c1EtGIF4DGE6upAbmM2juMJpxKI0tCA02AHHOgI46cWusHbCuPLsJlujMBXLmlDYQm0Ef950fB17N7I7+MqWUjvpX52Y0tvrCBpVQJ7TVxSv+l/SSNQmVzxD1aQjY32OVmvRU4xA7TiO53hPtXEdEV7PRMAF9jaczsitdiAtW3YTrvO8+TQQ//ENqjCDA1CNk2xo1WOhcvK5CZlhnGmhGSLfoQnr2PCoYz9/uFjXf0Lsd5jX3B0ft4gg==

On 12/29/20 8:36 PM, Jeremy Dawson wrote:

> I don't understand how this can be possible. Wouldn't you expect Coq to
> refuse to have a goal containing a type error? What would be happening
> here?

It's a type inference issue. If you use `Set Printing All` before `Show` it
will give you all implicit arguments, and then Check should work.

[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