coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type casting of a dependent type

From: Maximilian Wuttke <mwuttke97 AT posteo.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Type casting of a dependent type
Date: Mon, 28 Sep 2020 16:46:57 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mwuttke97 AT posteo.de; spf=Pass smtp.mailfrom=mwuttke97 AT posteo.de; spf=None smtp.helo=postmaster AT mout01.posteo.de
Ironport-phdr: 9a23:/qMpHx+eYsKzzP9uRHKM819IXTAuvvDOBiVQ1KB30uwcTK2v8tzYMVDF4r011RmVBNqdsawP1rSempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgdFiCCjbb5zIxm7rQTcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh7W/ZlMJwgqJYrhyvqRNwzIzbb52aOvdlYqPQfskXSXZdUstfVSFMBJ63YYsVD+oGOOZVt47zqEEBrBu/AAmsBefvyj5SiX/wwKY10/khER3a3AwjAd0FrXPZrND7NacPTeC10KrIwivHYv5Uwjr98I/Icgs9of6SWrJ8a9fexlc2Gg7Dk16fppDrMSmP2eQRr2iU8fBgVeS3hmAptw1/rDihy8Qoh4fGiIwZ1F7K+Dt2zos1J9C0VlB2bNC4HZZUtCyXOYR4Tt8+Tm12tis3xbwLt5C7ciYE1ZkqwQPUZf+fc4WQ/x7uV+acLS15iX9nYr6yiRe//VKhx+D8TsW501JHojBYntTDt30BzQLf5tabRvdn40us1yqD2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmEXxka+Walko9vWy5+T/ZbXmvYOcOJFzig3kL6shhNSzAeU+MgcQQ2iW4fmw2b7j8EHjQbhHjOc6n6fYvZzAJMkWpra1AwpP3YYi7xa/AS2m0NMdnXQfKVJEdg+Hj5T1O1HNPv/1CfWyjk+0kDds3PDGIqPuApLXInfejrjtZax95FJEyAov0dBf4IpZBa0GIPLqQ0P+qNjYDgIiPAGv2ObmCNB91psEVm6VA6+ZNrnSsV6S6e41LemMftxdhDGoIP88ovXqkHURmFkHfKDv04FERmq/G6FDKlWYZHvog94HWVgXohY9QaS+jUKfTSJQaiftd7o7/S02D8SqANGQFciWnLWd0XLjTdVtbWdcBwXUSCa6R8C/Q/4JLRmqDIpkmz0AW6KmTtZ4hwmprxP3zPxrI7iNo3BKhdfYzNFwotbru1Qy+DhzVpTP1maQUzkt2HsPXCM72+ZzrB4lkwvR4e1Dm/VdUOdrybZRSA5jbMzEyPdmBte0Vg+TJto=

On 28/09/2020 16:34, 劉弘毅 wrote:
> Moreover, I cannot unfold the "cast" function since it is defined with
> "Proof" and made opaque. Is it impossible to make this kind of comparison?

That is why I used `Defined.` instead of `Qed.`

[Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
- Re: [Coq-Club] Type casting of a dependent type, Maximilian Wuttke, 09/28/2020
  - Re: [Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
    - Re: [Coq-Club] Type casting of a dependent type, Adam Chlipala, 09/28/2020
      - Re: [Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
        
        Re: [Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
    - Re: [Coq-Club] Type casting of a dependent type, Maximilian Wuttke, 09/28/2020