Stream: Coq users

Topic: Search library


view this post on Zulip 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()

view this post on Zulip Paolo Giarrusso (Sep 12 2021 at 15:12):

That does not look like Coq, this is probably the wrong forum

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip zohaze (Sep 12 2021 at 17:43):

Is there any example ? (in case of matlab)

view this post on Zulip 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

view this post on Zulip zohaze (Sep 12 2021 at 17:54):

ok,thanks

view this post on Zulip 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: Jan 28 2023 at 06:30 UTC