Thomas Tuerk committed 288ed12

zip_same_length added to "list_extra", minor tweaks on hol-heap

Comments (0)

Files changed (3)


 open pred_setSimps pred_setTheory
 open finite_mapTheory
 open set_relationTheory
+open integerTheory intReduce;
 val _ = numLib.prefer_num();


-HOLHEAP = ../../hol-lib/lemheap
+HOLHEAP = ../../hol-lib/lemheap
+INCLUDES = ../../hol-lib


 declare compile_message find_non_pure = "find_non_pure is undefined, if no element with the property is in the list. Better use find."
+(* ------------------------- *)
+(* zip same length           *)
+(* ------------------------- *)
+val zip_same_length : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b) 
+let inline zip_same_length =
+declare compile_message zip_same_length = "zip_same_length is undefined, if the two lists have different lengths"
+declare hol target_rep function zip_same_length l1 l2 = `ZIP` (l1, l2)
+declare ocaml target_rep function zip_same_length = `List.combine` 
+assert zip_same_length_1 : (zip_same_length [(1:nat); 2;3;4;5] [(2:nat); 3;4;5;6] = [(1,2);(2,3);(3,4);(4,5);(5,6)])
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.