zohaze (Sep 12 2021 at 13:57): zohaze (Sep 12 2021 at 13:57):Which library I should include to read a color image? Like in python
image = cv2.imread('/home/pictures/1.jpg')
plt.imshow(image)
plt.show()
Paolo Giarrusso (Sep 12 2021 at 15:12):That does not look like Coq, this is probably the wrong forum
zohaze (Sep 12 2021 at 17:13):I mean how to read image in Coq , like other languages? I want to prove some properties of color image. But do't know how to have values of colors in 3d array against image.(know in metlab)
Karl Palmskog (Sep 12 2021 at 17:22):Coq is a pure language, so by default it doesn't have any way to input anything from the filesystem except compiled Coq code. People do write tools and extensions to generate Coq code with the data they want, though.
zohaze (Sep 12 2021 at 17:43):Is there any example ? (in case of matlab)
Karl Palmskog (Sep 12 2021 at 17:50):no idea about metlab (Matlab?), but for example the CompCert compiler has a tool which generates Coq code from C programs: https://github.com/AbsInt/CompCert/tree/master/exportclight
zohaze (Sep 12 2021 at 17:54):ok,thanks
Emilio Jesús Gallego Arias (Sep 13 2021 at 14:16):You can also generate a .v file with a constant that contains an array with the image.
Last updated: Sep 30 2023 at 06:01 UTC