Minor changes

Author: cmester0

engine/backends/coq/coq/coq_backend.ml

@@ -623,7 +623,7 @@ struct
              ^^ break 1))
         ^^ break 1
         ^^ CoqNotation.arguments (!^"Build_" ^^ name#p)
-             arguments_explicity_with_ty
+          arguments_explicity_without_ty (* arguments_explicity_with_ty *)
         ^^ concat_map_with ~pre:(break 1)
              (fun (ident, typ, attr) ->
                CoqNotation.arguments ident#p arguments_explicity_without_ty)
@@ -991,8 +991,10 @@ struct
           | "ge" -> "PartialOrd_f_ge"
           | "rem" -> "Rem_f_rem"
           | "add" -> "Add_f_add"
+          | "sub" -> "Sub_f_sub"
           | "mul" -> "Mul_f_mul"
           | "div" -> "Div_f_div"
+          | "index" -> "Index_f_index"
           | x -> x)
     end
 

examples/Cargo.lock

@@ -11,3 +11,5 @@ mod test_functions;
 mod test_instance;
 
 mod test_trait;
+
+mod test_arrays;

examples/coverage/src/lib.rs

@@ -0,0 +1,35 @@
+
+// // This function borrows a slice.
+// fn analyze_slice(slice: &[i32]) {
+//     let _ = slice[0];
+//     let _ = slice.len();
+// }
+
+// fn test(){
+//     // Fixed-size array (type signature is superfluous).
+//     let xs: [i32; 5] = [1, 2, 3, 4, 5];
+
+//     // All elements can be initialized to the same value.
+//     let ys: [i32; 500] = [0; 500];
+
+//     // Indexing starts at 0.
+//     let _ = xs[0];
+//     let _ = xs[1];
+
+//     // `len` returns the count of elements in the array.
+//     let _ = xs.len();
+
+//     // Arrays can be automatically borrowed as slices.
+//     analyze_slice(&xs);
+
+//     // Slices can point to a section of an array.
+//     // They are of the form [starting_index..ending_index].
+//     // `starting_index` is the first position in the slice.
+//     // `ending_index` is one more than the last position in the slice.
+//     analyze_slice(&ys[1 .. 4]);
+
+//     // Example of empty slice `&[]`:
+//     let empty_array: [u32; 0] = [];
+//     assert_eq!(&empty_array, &[]);
+//     assert_eq!(&empty_array, &[][..]); // Same but more verbose
+// }