coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] conversion from vector to list and back

From: Fritjof Bornebusch <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] conversion from vector to list and back
Date: Thu, 21 May 2020 14:18:53 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT gabriel-vm-2.zfn.uni-bremen.de
Ironport-phdr: 9a23:gfDVBhHEk+HMCQYuzs1ziZ1GYnF86YWxBRYc798ds5kLTJ7zrsywAkXT6L1XgUPTWs2DsrQY0reQ6vm5EjBfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmssAndq9QajYRtJ6sz1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhyhqRJh3oDaY46aO+Zjca7GYdMWWXBMUtpNWyBdAI6xaZYEAeobPeZfqonwv1sArQG/BQmwBuPvzTFIjWLr0K09yeQhFx/J0xc9H9IVrHvUrMj+OaAcUeCvzanI0TfDb/RY2Trm9YjIdBEhreiXUrJqb8XRzFcgFwXfglqNt4PoJjWY3fkCvGaH9eRvT/6vi3I5pAFrpDii3sQhhpXVio8by13J8SV0zYcxKNGlVkN2bt6qHptQuiyHM4Z4TcAvT3xotis4xLALvYK2cicExpkmxxPSavyJfYaO7xn+WuiRJjJ4i2hkeLK5nxuy8E6gyvf9VsauylpKoDBFn9/RvX4Ozxze8tWLR/Vy80u7xDqDyx7f5vtELEwoj6bXNpwszqYzm5YNq0jPADP6lUfsgKOIaEko5/Kk5uTnb7jgu5SSLZV7ihvkPaQrgsG/Afo3MgwJX2WD9uSzzqbs/Vf4QLpUiv06i7fZsJXDKcgFvKK4AgFV0oA55xaiCTem0c0UkmIdLF1bfRKIkY7pN0vTL//mFfu/glKsnyl3x/3eI7HsDJrAImLenLv9Y7px8U5RxBYpwdxC5Z9YErQBL+jyWk/1utzYFBg5MwmszubpEtV9158eWWCIAq+XK67SrFmI5uM2L+aXfo8apjP9JOYj5/L0kHA2h0cRfbO10psPdHC4AvNmLl2Fbnrrm9cNCHsFvg4jTOPxk1CCSj5SZ3OqX60m/D07CYSmDZ3CRo+3mrCB0j27TdVqYTVNDUnJGnP1fa2FXe0NYWScOJxPiDsBAJa7SpMj0h/mngjgzbdtM/Hf+mVMu4jiyNpy6cXOkxB3/yZ5CsmblW2AGTIn1lgUTiM7ifgs6Xd2zU2OhPAh3q5oUOdL7vYMaT8UcJ7Ry+shUYL9Uwjbf9qNDUijB4/gEz83CM83wpoEeUt4FtPkgh2Rh3P7UY9QrKSCAdkPyoyZ2nHwI8hnzHOfifs8iVhjSNFCMGCgwKJypVGKW9z51n6BnqPvTpwymTbX/T7en3eIvQRSSgN1XKODUX1NPkY=

Hi,

I was just playing around with vectors and lists and discoverd the following:

Definition BitVector_10 := Bvector (10).
Definition foo (bv : BitVector_10) : BitVector_10 := Vector.of_list
(Vector.to_list bv).

=> In environment
bv : BitVector_10
The term "Vector.of_list (Vector.to_list bv)" has type
"Vector.t bool (length (Vector.to_list bv))"
while it is expected to have type "BitVector_10".

The documentation assumes something different:
https://coq.inria.fr/library/Coq.Vectors.VectorDef.html
vector <=> list functions

Does someone know how to address the problem with function "foo"?

Best Regards,
--f.

[Coq-Club] conversion from vector to list and back, Fritjof Bornebusch, 05/21/2020
- Re: [Coq-Club] conversion from vector to list and back, Siegfried, 05/21/2020
- Re: [Coq-Club] conversion from vector to list and back, Maximilian Wuttke, 05/21/2020
  - Re: [Coq-Club] conversion from vector to list and back, Fritjof Bornebusch, 05/21/2020
    - Re: [Coq-Club] conversion from vector to list and back, Talia Ringer, 05/22/2020
      - Re: [Coq-Club] conversion from vector to list and back, Talia Ringer, 05/22/2020
        
        Re: [Coq-Club] conversion from vector to list and back, Fritjof Bornebusch, 05/22/2020