coq/theories/Vectors, branch masterThe formal proof systemadd results on to_list2021-03-16T20:06:35+00:00Olivier Laurent2020-12-23T19:36:37+00:00e444fe31f66a2a923f9f46affbb4731620ec901e
Explicitly annotate all hint declarations of the standard library.2020-11-16T11:28:27+00:00Pierre-Marie Pédrot2020-11-14T16:55:07+00:0068cd077344ce37db1a601079dbc4fdcae6c8d41f
By default Coq stdlib warnings raise an error, so this is really required.
By default Coq stdlib warnings raise an error, so this is really required.
Modify Vectors/VectorEq.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T23:30:39+00:004d4d2128d2dc761a1b3e002780b865f77fe61e67
Modify Vectors/VectorSpec.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T23:29:43+00:003191883b460747ad7eb68032f72b9228294f3f3f
Modify Vectors/VectorDef.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T23:04:25+00:00c3fd4e4e46b0681b2fd2bc1ade5dc489869a507a
Modify Vectors/Fin.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T23:03:25+00:00aab1a1280caca5a2e6b10f230c504771028aee2b
add properties of operations on vectors2020-04-11T09:37:53+00:00Olivier Laurent2020-04-03T16:42:22+00:008b9219a06fa72ec69ec404e97cf8c87de30f9965
Update headers in the whole code base.2020-03-18T11:15:43+00:00Théo Zimmermann2020-03-18T11:14:26+00:00a99776e10e0b2198d2b811ad82631111fb450f8a
Add headers to a few files which were missing them.
Add headers to a few files which were missing them.
edits per review2019-09-01T06:20:50+00:00Yishuai Li2019-09-01T06:00:06+00:00016c22454c6745ac753d7e376c9f457d6e934114
Vectors: lemmas about uncons and splitAt2019-09-01T06:10:00+00:00Yishuai Li2018-08-31T01:01:21+00:00ea23c93e33131216cff049a908a3e423dc704624
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>